Lean Together 2021

Thank you so much to Rob Lewis and Patrick Massot for organising Lean Together 2021! This annual Lean conference, like mathlib, seems to double in size every year. This year over 200 people registered, and even though it was all online and there were a lot of talks spanning everything from research level mathematics to hard-core computer science (so nobody would understand all of them), there still seemed to be between 50 and 100 people attending every talk. I attended all of them, but certainly didn’t follow all of them; I’ll discuss some the talks that I feel qualified to talk about. Anyone jealous that they missed out can catch up with essentially all of the talks on the leanprover-community youtube channel.

Most or all of the talks mentioned below have slides and/or video available. Check out the schedule for links.

Overview of some of the talks.

Do your theorems use all their assumptions? Is your theorem about fields actually true more generally for division rings? Or even rings? Or even semirings? Lean now has a linter which will check these things for you, written by Alex Best and showcased in his talk. This is important for Lean’s maths library because, like Bourbaki, we strive to prove theorems in the correct generality, and now we have a tool which checks that this is happening.

Floris van Doorn has formalised the theory of the Haar measure in Lean. This is the sort of thing which really excites me. Haar measure is a measure on a locally compact Hausdorff topological group which is translation-invariant. I read the proof of existence and uniqueness of Haar measure when I was teaching an old course on Tate’s thesis. The proof is long, and tricky in places, but fairly low-level. It’s just the kind of thing which one might imagine “sure this could be checked by a computer — in theory”. Floris has shown that with Lean it can be checked by a computer in practice. The systems work and this is why we mathematicians should be using them.

Heather Macbeth did something equally great even though to a non-expert it might look less impressive. She gave the n-sphere the structure of a manifold. The reason this is important is that it’s essentially the first non-trivial example of a manifold that we have. Manifolds are really complicated! Sorting out all the theory of charts took a while, and the fact that Heather can make a sphere into a manifold is, for me, strong evidence that the Lean analysts (Heather included) have got the set-up right. Future work: use the inverse function theorem to make zeros of functions in affine space into manifolds. This stuff is hard work. But it’s happening.

I remember when the world wide web was born. Academics made web pages, which consisted of text, pictures, and hyperlinks to more web pages. People could see the potential, but it took many more years before the web became accessible to the masses, and web pages became powerful and flexible tools. Ed Ayers talked about widgets, his addition to core Lean which enables pictures and links to be embedded in Lean output in VS Code, and enables the user to inspect the types of terms and subterms in Lean output, jump to definitions and more. This has got huge potential, and it will be interesting to see it realised. Students on the Xena Discord have already used them to make graphical logic games. There is more to come here.

Chris Hughes talked about his group theory tactic. It is now fast, and solves problems in group theory of the form “show this finite set of equations implies this one”. In fact he has written several tactics which do this; time will tell which techniques are most useful in practice.

The blue-eyed islanders puzzle is something we’ve talked about on the blog before. One has to think hard about how to formalise the question mathematically. Paula Neeley talked about her work formalising a framework for dynamic epistemic logic in Lean, which will enable us to work on questions such as this in a much less ad-hoc way.

Kenny Lau talked about his work formalising the Deligne/Fontaine–Wintenberger/Scholze theory of tilting, part of his Imperial MSc project. Working with Kenny has been an interesting experience. When Massot, Commelin and I were working on perfectoid spaces we formalised a very general definition of a valuation, taking values in an arbitrary totally ordered abelian group with zero; this is what is needed to formalise the theory of adic spaces. For the theory of tilting, Kenny and I have realised that actually we need an even more general theory — in Deligne’s paper on fields of characteristic p which are “limits” of fields of characteristic zero, he uses valuations taking values in certain monoids with zero. I’ve been working on refactoring the definition and we are nearly there.

Yasmine Sharoda talked about her work on building algebraic hierarchies. This is a very “computer science” problem, and quite hard to explain to mathematicians. Basically mathematicians carry around their head a big web of trivial facts — a scheme is by definition a locally ringed space, which is by definition a ringed space, which is by definition a topological space. A ring is by definition a semiring, a monoid, an additive group, and additive semigroup, and so on. Computer programs like Lean need some kind of organisational principle to mean that mathematicians can move freely between these ideas without noticing that they’re doing so — either that, or libraries suddenly experience an irrelevant growth factor when the theorem that has to be proved for additive monoids, groups, semirings, rings, division rings, integral domains and fields. This is a problem which I do not understand the details of, but I have now seen sufficiently many talks on it to understand that computer scientists are concerned about this issue. I think they are in some sense planning for the future though — Lean has no trouble working with schemes or fields right now.

Adam Topaz talked about his work formalising theorems in anabelian geometry. There is a problem here — beyond a certain point one needs the theorems of local and global class field theory, and the proofs of these things are long and difficult. My proposed solution: let’s just formalise the statements, and worry about the proofs later. The sooner we start doing interesting maths like what Adam is attempting, the better.

Peter Nelson talked about formalising matroids. This is hard, for the wrong reasons. It seems to me that type theory is ideal if you are formalising things which can be expressed in the language of category theory (i.e., if you have objects and morphisms). Matroids are combinatorial objects and a fundamental construction stressed by Peter was that of a minor of a matroid. This is some kind of subobject, but there seems to me to be no natural general notion of a morphism of matroids. One needs to talk about minors of minors freely, and this can start to get convoluted if one is not careful. One wonders whether this kind of stuff would be easier to do in a set-theory based system. One approach would be the “Coq odd order theorem” approach, where you work in a large matroid and everything is some kind of submatroid of this (groups in the Coq odd order work were all subgroups of a large ambient group which had no mathematical relevance — it was just a way to hold things together). But I really don’t want to go down this route. Kenny Lau seems to have solved the problem of subfields of subfields using an elegant is_scalar_tower structure; I wonder if a similar idea can be used here. I’ve realised that matroids are a great example to bear in mind when one is thinking about solving these type-theoretic issues practically.

Marie Kerjean talked about her work on the foundations of complex analysis in Coq. We have essentially no complex analysis in Lean, although there is a ton of the stuff in Isabelle/HOL. I’m sure that the Lean community will be able to learn from her efforts when we turn our attention to these matters.

Damiano Testa is well on the way to proving that the image of a constructible set under a finite type morphism of schemes is constructible. What we are missing right now is the definition of a product of schemes, so he has been working in the affine case for now and has essentially finished that part. I remember ploughing through the construction of a product of schemes in Hartshorne when I was a PhD student. It will be fun to do it in Lean — this is the kind of stuff which should turn out nicely.

Amelia Livingston talked about the nature of universal objects. This talk had some ideas in which I’m still wrestling with. Here’s a funny observation, which goes back to Patrick Massot. Say is a commutative ring and is a multiplicative subset. How does one prove that the kernel of the canonical map is the annihilator of ? This can’t be hard. I don’t know how to deduce it directly from the universal property of though. The only proof I know involves having to make the usual explicit construction of as and to prove it for this specific model. Is this a surprise? Well, if I told you that you could assume that the real numbers were a complete ordered archimedean field (the universal property) and then I asked you to prove a fact about the real numbers, and it turned out that to prove it you had to use the construction of the reals as, say, Cauchy sequences, I think you would be surprised. The universal property is supposed to characterise the object up to unique isomorphism and save us the trouble of having to build it every time we need it. Amelia in her talk explained that she had discovered something even weirder. Despite the fact that mathlib has both a construction of the tensor algebra of an -module and a proof of its universal property, the statement that is injective seemed to follow from neither the universal property nor the construction in mathlib, so she had to make a second construction. This is like coming up with an assertion about the real numbers which you can’t prove from the axioms, or from the construction as Cauchy sequences, so you have to make them again as Dedekind cuts before the result becomes clear. What is going on here? Amelia is working on Koszul complexes in Lean as part of her MSc project and this is where the issue came up.

Alena Gusakov, one of the moderators of the Xena Discord, talked about her work with Bhavik Mehta (another moderator) and Kyle Miller on formalising all the forms of Hall’s Marriage Theorem that you’ve ever heard of. Graph theory is another one of these objects which don’t naturally fall into the arms of category theory (what is a morphism of graphs? I did an entire graph theory course as an undergraduate and saw some deep and tricky theorems, but this concept was not mentioned once). Like matroids, graphs get manipulated (edges get removed or contracted) rather than morphismed, and for some reason this makes them more difficult to use in type theory. What is going on here? This deserves a better explanation.

Thomas Browning and Patrick Lutz are PhD students at UC Berkeley, and, building on work of undergraduates at Imperial, they have formalised the fundamental theorem of Galois theory in Lean and are on their way to proving insolvability of the quintic, problem 16 of the Formalizing 100 Theorems challenge. To my astonishment, this is one of the problems which has not been formalised in any theorem prover, although Cyril Cohen tells me that Sophie Bernard, Pierre-Yves Strub, Assia Mahboubi and him are working on it in Coq. [Update: the Coq team have finished!]

There were other talks, but on things I understand less well. Yury Kudryashov talked about dynamics of the circle. Mario Carneiro talked about Metamath 1. Vaibhav Karve talked about axiomatising various theories he’s been thinking about such as model theory. Jannis Limberg talked about tactic-writing. Stan Polu and Jason Rute talked about Lean and AI (including demonstrations of an AI program solving levels of the natural number game!), and Koundinya Vajjha, Joe Hendrix and Logan Murphy all talked about formalisation projects which are way beyond my area of expertise.

Oh, and Leo de Moura and Sebastian Ullrich released Lean 4, and gave several talks demonstrating what it did. A lot of people were excited about this, but for me Lean 4 is currently unusable (there is no maths in it). I’m not going back to proving directly from the axioms of a ring, and unfortunately I am not capable of doing any of the things which are required in order to make Lean 4 have a ring tactic. However, there were a bunch of people at the conference who clearly are capable of doing these things, including Daniel Selsam, who is thinking about how one can import compiled Lean 3 files into Lean 4 (Lean 3 and Lean 4 share the same type theory). Once we have this, I will be extremely interested. And hopefully it won’t be too long.

Afterthoughts

I counted no fewer than four occurrences of the phrase “it’s fun!” in various slides in the talks, and there could have been more. This was within the context of people asking “why formalise X?”. Typically it would be one of several answers. I did not speak at the conference, but had I done so I suspect there would have been a fifth occurrence. Imagine people putting “it’s fun!” in the slides in a traditional number theory talk! Sure it’s interesting to do research into modern number theory — this was something I did with great verve and enthusiasm for nearly 25 years, and I suspect I probably was having fun some of the time. But “fun” is not a word I ever remember running into in a presentation. Why are people highlighting it here? Perhaps we are more conscious of the fact. Is it guilt that it’s supposed to be work but actually we’re really enjoying it? Sometimes I wake up in the middle of the night and want to get out of bed and formalise. Maybe “it’s addictive” is closer to the truth?

Whatever the real reason is behind it, Lean’s maths library continues to grow. In 2020 several more professional number theorists started formalising in Lean (Riccardo Brasca, Damiano Testa, Marc Masdeu, Filippo Nuccio) and stuff like the theory of cyclotomic polynomials has just appeared organically in mathlib as a result of this. Johan Commelin continues to work tirelessly on this stuff too; my PhD student Ashvni needed Bernoulli numbers for a project she’s working on, and it turned out that Johan had formalised them a few months earlier. As long as things like this keep happening, mathlib will more and more start to look like a respectable basis for a lot of MSc level mathematics. Perhaps my forthcoming Lean course for PhD students (starting in 10 days; more info to come) will get us a few more converts.

Thanks once again to Patrick and Rob for organising the conference.

My daughter says she hasn’t got any art ready, so here’s something one of my sons did a few years ago when he was learning Blender.