Which mathematical definitions should be formalised in Lean?

Kevin Buzzard 09/21/2018. 14 answers, 2.028 views

The question.

Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?

Examples.

In the current stable version of the Lean Theorem Prover, topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds -- maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and today we got modular forms. There is a sort of an indication of where we are.

What else should we be doing? What should we work on next?

Some background.

The Lean theorem prover is a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language. You can read my personal thoughts on why I believe this question is timely and important for the pure mathematics community.

Over the last year I have become increasingly interested in the mathematics library for the Lean theorem prover, a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language.

My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. Let's get one thing straight -- formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.

But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Tom Hales' formal abstracts project plans to formalise the statements of new theorems as they come out -- look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in Lean and send it to Tom Hales! If you need hints about how to do that, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.

We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.

community wiki 09/21/2018.

Basics of differential geometry:

1. Definitions of manifold, tangent and tensor bundles
2. Basic theorems:
• Frobenius theorem
• Poincare lemma
• Implicit function theorem
3. Basics of Riemannian geometry

Benjamin Steinberg 09/21/2018.

I would like to see that Statement of the Classification of Finite Simple Groups formalized. And then I would like to see the proof formalized. Many people use the theorem as a black box. The first generation human proof is too big for people who are not working on the second generation and third generation proofs to completely understand and it would be a huge service to the mathematical community to formalize this, as was done for the Odd Order Theorem.

community wiki 09/21/2018.

I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the number field case.

I am currently unclear on whether there is a way to rigorously formalise the statement of the full Global Langlands Reciprocity Conjecture, or whether it is just supposed to be a "philosophy" which implies functoriality. I wish I understood more of Jim Arthur's paper on the subject.

community wiki 09/21/2018.

Maybe a formalization of homological algebra would be interesting? There are many objects that appear to depend on a choice of an infinite projective (or injective) resolution, but in fact need only finitely many terms, and are independent of which resolution is chosen.

In particular, I suggest formalizing the $$\mathrm{Ext}$$ and $$\mathrm{Tor}$$ functors for modules over a Noetherian ring.

François Brunault 09/21/2018.

I would really like to see motives formalized. Although motives were in the beginning more a "philosophy" (dating back at least to Grothendieck), the situation has evolved and thanks to Beilinson's insights and the work of Voevodsky (among others), we now have working definitions for the category of mixed motives (technically this is a triangulated category: it still remains to define a $$t$$-structure on this category in order to get an abelian category of mixed motives). Of course, the philosophy is still there and the informal point of view is both necessary and very motivating, but the point is that things have become much more precise. As an application or motivation for this formalization, I think of the conjectures about the transcendence of periods (in the sense of Kontsevich and Zagier). These conjectures naturally fit in and extend to the framework of motives, where one tries to describe all the algebraic relations between periods (or regulators) associated to one or several given motives.

I feel that I should try to give a flavour of what motives look like. Very roughly, the motive associated to an algebraic variety $$X$$ is an abstract version of the cohomology group $$H^i(X)$$. Motives are universal in the sense that applying various realization functors we recover the usual cohomologies. Smooth proper varieties give rise to pure motives, while general varieties give rise to mixed motives (basically, non-trivial extensions of pure motives). Voevodsky's published work deals with algebraic varieties over a field, but we now have definitions for (triangulated) mixed motives over a pretty much arbitrary base scheme, and with arbitrary coefficient rings.

Broadly speaking, the theory of motives has an heavy formalism but this is precisely where computers may be helpful. The actual construction relies in particular on homological and homotopical algebra, so I guess one would need to formalize this first, which could be a lot of (interesting!) work. Of course, it would also build on the formalization of schemes.

I should add that although the theory of motives is generally considered as difficult, formalizing them could help in making it more accessible. Namely, it is the kind of theory which has gone very far, but the layman struggles to even find the definitions. The conjectures in transcendence number theory that I mentioned are very appealing, but it's hard to make them precise, in the sense of finding and understanding the relevant literature. Of course, the experts (not me) know how to formulate things or at least have a clear view, but somehow I feel that the access to this knowledge is difficult (there are a number of excellent references on motives though). I hope that having a formalization would encourage interested people to actually learn more about motives.

Neil Strickland 09/22/2018.

Here is a list of things that I would like to see formalised, slightly modified from the list that I was using at Schloss Dagstuhl Seminar 18341. All of these things should be trivial for the experts. However, I would like to see formalisations with extensive explanation and annotation, written from the point of view of mathematicians who might want to use Lean, not from the point of view of developers of proof assistants.

1. Prove that $$2+2=4$$. Key points: basic boilerplate at the top of the file, basic grammar of stating and proving, how to interact with the proof assistant.
2. Prove that there are infinitely many primes. Key points: more basic grammar, how to search and refer to existing libraries, how to write a proof by contradiction, how to write a proof that constructs a witness to an existential statement.
3. Set up the basic facts about the group of units of a commutative ring, and prove that $$\mathbb{Z}^\times=\{1,-1\}$$. Key points: the basic framework for dealing with algebraic structures such as rings and groups. The basic framework for dealing with substructures defined by a condition such as invertibility. The framework for dealing with chains of algebraic identities. Where to look in the library for facts about $$\mathbb{Z}$$. How to refer to the standard ring structure of $$\mathbb{Z}$$.
4. Set up the theory the ideal of nilpotent elements in a commutative ring $$R$$. Prove that $$\text{Nil}(R)$$ is an ideal and that $$\text{Nil}(\mathbb{Z}/4)=\{0,2\}$$ and that $$\text{Nil}(R/\text{Nil}(R))=\{0\}$$. Key points: the basic framework for quotient structures. The framework for dealing with $$\mathbb{Z}/n$$ (which might be defined as a quotient ring, or as the set $$\{0,\dotsc,n-1\}\subset\mathbb{N}$$). The framework for dealing with ring homomorphisms, including the projection $$\mathbb{Z}\to\mathbb{Z}/n$$. Indexed sums in general, and the binomial expansion.
5. Given a finite set $$A$$ (with decidable equality), construct the poset of partitions of $$A$$, as an instance of some well-structured theory of finite posets. Prove that if $$|A|=3$$ then $$|\text{Part}(A)|=5$$. Key points: the basic framework for dealing with finiteness and decidability.

I have been working on this myself, doing Coq+sseflect, Isabelle+HOL-algebra and Lean in parallel, but so far I have spent less time on Lean than with the other two, so I have only looked at tasks 1 and 2 in Lean. I spent about a week on this directly after Dagstuhl but then had to turn to other things; I hope to get back to it in a week or two. Of course all the real mathematical issues are simple, but apparently trivial points about the software framework can easily absorb enormous amounts of time. If anyone wants to send me Lean code then I would be grateful.

I will also say that the main issue in promoting the use of Lean is not the presence or absence of formalisations of your favourite bits of mathematics.

1. It is not possible to get a usable installation of Lean + library under Windows without following instructions in Kevin's blog post, which is hard to find unless a well-informed person directs you there. If you get anything wrong, then the error messages are not helpful. You first have to install MSYS + various packages, totalling nearly 1GB. As far as I can tell this could be avoided by restructuring a couple of files in the Lean C++ code to use the appropriate Windows system calls rather than starting an external process. That would also let you install Lean properly in C:\Program Files, rather than having to use a path without spaces. The lead developer has told me that he does not see it as a priority to fix any of this. All this is slightly ironic given that the project is funded by Microsoft.
2. Although there is a lot that is very good about the existing documentation, it is clearly not written from the point of view of a mathematician who is interested in using Lean to help check proof of new things.

community wiki 09/22/2018.

I would like to see classical representation theory and Lie theory formalised:

• Representations of finite groups
• Classification of semisimple Lie algebras (over $$\bar{k}$$) and their finite-dimensional representations.

community wiki 09/21/2018.

Here are ideas that might be the type that you are looking for, some with more analytic flavor: formalize the statements of

(1) The Mostow Rigidity Theorem.

(2) The existence of Brownian motion.

(3) The Weyl law for the asymptotic behavior of the number of eigenvalues of the Laplace operator on a compact Riemannian manifold.

community wiki 09/21/2018.

This may be non-interesting or way off-base, but: I would love to see some way of formalizing the notion of "the category of real Banach spaces and bounded linear maps, in a world without assuming the Hahn-Banach theorem". The point is that some short exact sequences seem to split in the "usual category" of Banach spaces, without splitting in the category mentioned above, and this affects whether various Banach spaces are isomorphic or not.

It might then be possible to apply a properly homological point of view to questions in functional analysis that normally get stated loosely as "yes, well we know X happens, but that needs Axiom of Choice".

community wiki 09/21/2018.

Something which shouldn't require completeness: the Tsirelson norm on the space of finitely supported real-valued sequences. (Well, more precisely, the norm defined in Figiel and Johnson's paper http://www.numdam.org/item?id=CM_1974__29_2_179_0 ).

Thomas Kojar 09/22/2018.

Here are some definitions from analysis and probability:

• Many measure theory concepts follow clear axiomatic rules. One quick search gave Formalization of Measure Theory.
• Many commonly used functional spaces such as $$Sobolev$$ and $$H\ddot{o}lder$$ would be interesting to see eventually. A lot of calculus definitions and results seem to have been formalized already see

I am guessing one can start from them.

community wiki 09/21/2018.

I propose formalizing the definition of a Turing Machine, and hence decidable/computable languages.

(That said, a paper by Asperti and Ricciotti has already described doing it for the Matita Theorem Prover.)

community wiki 09/22/2018.
• Basic differential topology, basic Morse theory
• Category theory and standard theorems (Yoneda lemma, adjoint functor theorem, etc.)
• Simplicial sets
• Basic homotopy theory
• Some models of $$(\infty,n)$$-categories, and their equivalences

It would be amazing if we could formalise some version of the cobordism hypothesis, which connects Morse theory and $$(\infty,n)$$-category theory. At least the statement should be feasible.

community wiki 09/21/2018.

I think it would be great to have the Multiradial Representation of Inter-universal Teichmüller Theory, as in this: