137
$\begingroup$

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 sort of thing is timely and important for the pure mathematics community. Other formal proof verification software exists (Coq, Isabelle, Mizar...). I am very ignorant when it comes to other theorem provers and feel like I would like to see a comparison of where they all are.

Over the last year I have become increasingly interested in Lean's mathematics library, because it contains a bunch of what I as a number theorist regard as "normal mathematics". No issues with constructivism, the axiom of choice, quotients by equivalence relations, the law of the excluded middle or anything. 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. These paragraphs are an attempt to give an update to the community.

Let's start by getting 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 formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki in our spare time and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.

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. Whether it happens in Lean or one of the other systems -- time will tell. Tom Hales' formal abstracts project plans to formalise the statements of new theorems (in Lean) 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 a theorem prover and send it to Tom Hales! If you need hints about how to do that in Lean, 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.

$\endgroup$
36
  • 11
    $\begingroup$ This is not answering your question but related. I think it would be a huge service for the community to have a theorem prover formalize the classification of finite simple groups. Unlike Fermat's last theorem, the human proofs seem too big for people who have not dedicated their lives to it to really understand it but at the same time people use it constantly. $\endgroup$ Sep 21, 2018 at 13:41
  • 8
    $\begingroup$ Also, do you have things like formal power series? How much combinatorics is there? Are there good techniques for using some of the common abuses of notation (e.g., "invisible" inclusion maps), or does one have to learn to "think like the type system"? $\endgroup$ Sep 21, 2018 at 19:30
  • 14
    $\begingroup$ One of the criticisms of Lean on the blog of Hales is incredible: "Lean is not backwards compatible. Lean 3 broke the Lean 2 libraries, and old libraries still haven’t been ported to Lean 3. After nearly 2 years, it doesn’t look like that will ever happen. Instead new libraries are being built at great cost. Lean 4 is guaranteed to break the Lean 3 libraries when it arrives." So a big chunk of your work may be wrecked when the next version of Lean comes out. $\endgroup$
    – KConrad
    Sep 21, 2018 at 22:29
  • 13
    $\begingroup$ @ScottMorrison I know nothing about theorem prover systems, but it seems like a stupendously bone-headed idea to create a system with this type of "feature" at every single upgrade. $\endgroup$
    – KConrad
    Sep 22, 2018 at 1:46
  • 8
    $\begingroup$ Link to the meta discussion $\endgroup$ Sep 22, 2018 at 13:06

28 Answers 28

56
$\begingroup$

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.

$\endgroup$
8
  • 27
    $\begingroup$ If you want the proof formalized then you need to come up with $100,000,000 of grant money to pay for the staff. If you want the statement formalised then a first step is to find someone who knows precise definitions of all of the exceptional groups and tell them to come and explain them on the Zulip chat. It would be very interesting to see how far we would get. $\endgroup$ Sep 21, 2018 at 17:46
  • 20
    $\begingroup$ I can't say I have that money. $\endgroup$ Sep 21, 2018 at 19:51
  • 4
    $\begingroup$ @KevinBuzzard I actually asked a question about this with the intent of formalizing the statement, and I got some great answers. In particular, it turns out there is a book devoted to this topic, which is well written and explains all the exceptional groups. $\endgroup$ Sep 22, 2018 at 4:04
  • 8
    $\begingroup$ @KevinBuzzard: $100m? -- Well, you'd need to convince a funding agency that a formalization of the proof of the CFSG is certainly not worth less than a single football player! $\endgroup$
    – Stefan Kohl
    Sep 23, 2018 at 22:36
  • 2
    $\begingroup$ :-) This figure is only a stab in the dark. But I think the two volumes of the odd order theorem took a team of about 10 people about 6 years, and we're on...what? over 10 volumes for the classification and counting? With more still in the pipeline? $\endgroup$ Sep 23, 2018 at 23:38
43
$\begingroup$

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.

UPDATE: There has been some recent activity aiming to improve the installation process. You can read about it at https://github.com/leanprover/mathlib/blob/master/docs/elan.md. (I haven't tried it myself.)

$\endgroup$
13
  • 1
    $\begingroup$ Neil, all of what you say is easily do-able in Lean and mathlib, and most of it is already done in some form (although it may not be at all clear where to look). You are clearly interested in the pedagogy as well as the objects. I am very interested in teaching with Lean at the minute and might try to take up some of what you say as a challenge project for our incoming first years. $\endgroup$ Sep 22, 2018 at 13:14
  • 6
    $\begingroup$ PS I totally agree about installation being hell. Our first years will be using cocalc. William Stein got Lean working on it! $\endgroup$ Sep 22, 2018 at 13:15
  • 2
    $\begingroup$ @darijgrinberg ssreflect installation was a total nightmare in the past, but is much better now; the only issue is that the current version of ssreflect complains about Coq 8.8.1 so you have to install 8.8.0 instead. And Assia Mahboubi's book (math-comp.github.io/mcb) is a massive step forwards for the usability of ssreflect. But I agree that standard ssreflect style favours terseness over comprehensibility to a striking extent. $\endgroup$ Sep 23, 2018 at 5:45
  • 2
    $\begingroup$ @darijgrinberg There is a Windows installer at github.com/math-comp/math-comp/releases $\endgroup$ Sep 23, 2018 at 5:57
  • 2
    $\begingroup$ I strongly agree with the second set of points, and more generally the problem installing and getting everything (including the math library!) to work, where the instructions are self-contained. I've tried twice and given up - perhaps I should have been getting on the zulip chat and bothering people there about it, but I wasn't that invested in getting it to work. I didn't have that blog post though, and I will try that to see what happens. $\endgroup$ Sep 24, 2018 at 22:31
42
$\begingroup$

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
$\endgroup$
9
  • 3
    $\begingroup$ We are a long way from these now. The person to talk to about these is Patrick Massot. He is a geometer in Orsay who knows a lot about this stuff. $\endgroup$ Sep 21, 2018 at 17:44
  • 17
    $\begingroup$ @KevinBuzzard Why are we a long way from these? $\endgroup$
    – Kenny Lau
    Sep 21, 2018 at 19:09
  • 2
    $\begingroup$ All these topics is classical material that is known for $\ge 60$ years and underlying the topic of a large number of mathematicians. $\endgroup$
    – YCor
    Sep 21, 2018 at 20:50
  • 12
    $\begingroup$ Kenny, Patrick told me that he was genuinely surprised when he started formalising manifolds, how much stuff was "trivial and left to the reader" and turned out to have a little content. I am not sure of the present state of his formalisation of manifolds but I know that we are working on them. As you know, we have tensor products (you wrote them) so tensor bundles shouldn't be too hard after that. But the analysis is harder. Implicit function theorem -- I feel a long way from this sort of standard undergraduate analysis right now -- I mean, nobody is driving the theory yet. $\endgroup$ Sep 21, 2018 at 21:43
  • 12
    $\begingroup$ I think this kind of information is very valuable for formalizers even if it is far off. For people not working in the field, it is sometimes hard to gauge what is "common and general knowledge" for graduate and research level mathematicians. The stuff you think is basic and essential and all the formalizers think is a long shot is just where I think this list should target. $\endgroup$ Sep 22, 2018 at 4:28
20
$\begingroup$

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.
$\endgroup$
2
  • 4
    $\begingroup$ I would like to see the statement of the classification of connected reductive algebraic groups over an algebraically closed field because I've realised that this sort of stuff will be useful for both the finite simple group idea and the project to formalise Langlands' philosophy. $\endgroup$ Sep 22, 2018 at 8:32
  • 2
    $\begingroup$ The statement of the classification of semisimple Lie algebra has been done in Lean: gist.github.com/ocfnash/f3e3ca8eb24689dc3cb7b48de70439e6 $\endgroup$
    – jmc
    Nov 2, 2021 at 8:30
19
$\begingroup$

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.

$\endgroup$
8
  • 1
    $\begingroup$ The HoTT branch is in limbo at the moment --- it was only compatible with Lean 2. The Lean/HoTT people have some ideas about how to get started again, but for the most part I think they've decided to wait for Lean 4. (No expectation that it will be easier there, I think, just to avoid having a moving target.) $\endgroup$ Sep 22, 2018 at 0:21
  • 5
    $\begingroup$ @HarryGindi HoTT wouldn't be particularly useful here either, though, even if it wasn't caught up in sociological problems. HoTT only formalizes synthetic notions of homotopy, which only connect to what a geometer would call "real" homotopy theory at the metatheory level. Kevin is talking here about formalizing mathematics "the conventional way", which relies on traditional methods of point-set topology and the like. (There are people working on ways of connecting homotopy theory with its synthetic counterpart, but I think these also require new axioms, so I don't think it will help.) $\endgroup$ Sep 22, 2018 at 4:12
  • 4
    $\begingroup$ I think that Ext and Tor are a really excellent idea, they are accessible definitions and we need group cohomology for other reasons too. $\endgroup$ Sep 22, 2018 at 8:36
  • 9
    $\begingroup$ I would have expected that the best 'conventional' non-HoTT way of formalising homotopy theory of the kind relevant here would make use of simplicial methods, not topology. I don't know much about this project, but I'd love to see a proper Bourbaki-like treatment of simplicial things in a computer formalisation system. $\endgroup$ Sep 22, 2018 at 13:23
  • 1
    $\begingroup$ A Bourbaki-like treatment of simplicial things is most definitely within our grasp. We just need the person-power. $\endgroup$ Sep 23, 2018 at 20:45
18
$\begingroup$

Graphical calculus in monoidal categories with extra structure.

A lot of proofs in category theory are done graphically. There are even graphical proof assistants like Globular. Lean needs to make a connection to these eventually, so we can give rigorous graphical proofs.

This is not just about the library, but also additional tooling is required that e.g. transforms certain Lean quantities into diagrams in some format, and vice versa.

$\endgroup$
18
$\begingroup$

The other answers given here so far are interesting and colourful, but I'm proposing a strategic answer, drawing on the wisdom of (pre-existing) crowds. Here are several lists of core articles on Wikipedia, increasingly diffuse, but with more technical details in the longer lists.

  • 53 core articles (many but not all of these are already in Lean)
  • 300 core articles (including those above)
  • 481 core articles (including those above -- and, incidentally, including sheaves! -- this is what I'd suggest as the first-draft checklist for Lean, even if some of them get a WONTFIX status)

If the corresponding definitions and theorems were all in place, then I think various "wish list" items could be pursued more straightforwardly. Furthermore, many of these are topics that undergraduates could tackle, which would tend to increase the size of the pool of trained people for tackling more mathematically difficult topics later.

$\endgroup$
1
  • 2
    $\begingroup$ That's a neat idea -- thanks! We got logarithm yesterday :-) so I think we now cover the basics. Geometry (in the sense of the 53 core articles page) -- we don't have anything specific to R^2 or R^3 like squares or tetrahedra. As for "other" we have some but not all. Thanks for the list! $\endgroup$ Sep 25, 2018 at 13:29
16
$\begingroup$

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.

$\endgroup$
2
  • 2
    $\begingroup$ How about a formal definition of the local or global Weil group? Have you got that already? $\endgroup$
    – Marty
    Sep 21, 2018 at 17:44
  • $\begingroup$ The Weil groups are a far more accessible target. We have the p-adic numbers and it will be trivial to get general p-adic fields. We are working on Galois theory and algebraic closures. Once we have algebraic closures we can get local Weil groups on the cheap by saying that they're the elements in the local Galois group which act as raising to an integer power on a bunch of roots of unity. $\endgroup$ Sep 21, 2018 at 17:55
13
$\begingroup$

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.

$\endgroup$
8
  • 1
    $\begingroup$ I would love to work on this! Concretely, in Lean we have a definition of schemes (but it needs a cleanup), and we are quite close to the definition of Grothendieck topologies. We do not yet have a category of schemes and there is currently no definition of smooth/projective/etale/fppf/whatever morphisms. This should give you a bit of a feeling of where we stand. I think Voevodsky motives might actually be easier to formalise then Chow motives. But motives with transfer will probably be hard. $\endgroup$
    – jmc
    Sep 21, 2018 at 16:57
  • 2
    $\begingroup$ I have this vague idea that there are lots of different definitions of a motive which are only equivalent if you assume the Hodge conjecture and/or the Tate conjecture. I might be out of date though. If the word means different things to different people then this is a really good reason to formalise a definition -- so people can refer to it precisely and then we will have a better idea about what everyone is talking about. $\endgroup$ Sep 21, 2018 at 21:45
  • $\begingroup$ @jmc I'm glad you like this suggestion! Defining étale cohomology indeed looks like a good direction. $\endgroup$ Sep 21, 2018 at 22:54
  • $\begingroup$ @KevinBuzzard: There are indeed many definitions of motives, and relating them means proving hard theorems. I guess you refer to Grothendieck vs Chow motives: both are categories of pure motives and their definitions are standard. Regarding the more recent theory of mixed motives, as far as I know (not so much) there are two ways to define them: one using algebraic correspondences (Voevodsky) and one using $\mathbf{A}^1$-homotopy theory (Morel-Voevodsky). In any case morphisms of schemes are needed. $\endgroup$ Sep 21, 2018 at 22:58
  • 3
    $\begingroup$ It is manifestly clear that all the different ways of defining pure and mixed motives, and the relationship between them, are "known to the expert", and probably passed down from supervisor to student, perhaps with reference to a survey article which is now N years old. Why not store the most important parts of the state of the art in Lean instead? $\endgroup$ Sep 22, 2018 at 13:10
12
$\begingroup$
  • 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.

$\endgroup$
8
  • 2
    $\begingroup$ Category theory is growing fast in Lean. Yoneda is there, adjoint functors are almost there. Definition of simplicial sets and singular complexes has been done. But e.g., Eilenberg-Steenrod axioms haven't been done. $\endgroup$
    – jmc
    Sep 22, 2018 at 10:30
  • 3
    $\begingroup$ One thing I'd really like to do (and have thought a little about off-and-on but not seriously) is formalizing the proof of just the $(\infty,1)$ version of the cobordism hypothesis. $\endgroup$ Sep 22, 2018 at 22:53
  • $\begingroup$ @NoahSnyder, please do! If you start this open-source, I'll try and contribute! $\endgroup$ Sep 23, 2018 at 8:45
  • $\begingroup$ @NoahSnyder formalising stuff is now much much easier than it used to be. Choose Lean, or maybe another system if you prefer, and start asking about how it can be done. Lean has a bunch of category theory with more to come. The proofs of things like Yoneda is one command which translates to "just go ahead and chase the diagram". $\endgroup$ Sep 23, 2018 at 20:49
  • $\begingroup$ Locally presentable categories and combinatorial model categories please. Is it feasible ? I am actually discovering this thread and know nothing about Lean. $\endgroup$ Sep 25, 2018 at 12:26
12
$\begingroup$

As much a question as a suggestion, but now that a scheme is defined, is there a plan to move forward on EGA-style algebraic geometry? Is it feasible that someone (or many someones) could just plow through the Stacks project tag by tag, or are there some basic difficulties?

$\endgroup$
6
  • 3
    $\begingroup$ We did schemes, and the proof that an affine scheme was a scheme(!), and by this point I was convinced that it would in theory be possible to do all of EGA but that it would take many years. I think that digitising the stacks project would be a wonderful project, but who would fund it? $\endgroup$ Sep 23, 2018 at 20:47
  • $\begingroup$ I think it would either take many years, or many someones. $\endgroup$
    – jmc
    Sep 24, 2018 at 3:26
  • 4
    $\begingroup$ Just a wild idea: Maybe it'd be worthwhile to formalize synthetic scheme theory as opposed to traditional scheme theory layered upon topology and sheaf theory, similar to how it's worthwhile to formalize synthetic homotopy type theory. $\endgroup$ Sep 24, 2018 at 16:24
  • $\begingroup$ @IngoBlechschmidt Is there already a theory of "synthetic" scheme theory somewhere? I guess HoTT has the advantage that it fits nicely into Martin-Löf type theory, but I don't know if a similar claim follows for scheme theory, and even just discovering a reasonably complete/expressive language for scheme theory would be a major contribution. $\endgroup$ Sep 27, 2018 at 2:29
  • $\begingroup$ @Mario: Yes, a few beginnings are described on pages 11ff. of these notes of mine. However, it wasn't developed with HoTT in mind, that is, it's strictly one-categorical and no higher homotopies are in sight. $\endgroup$ Sep 27, 2018 at 19:22
10
$\begingroup$

Here are some definitions from analysis and probability:

$\endgroup$
1
  • 3
    $\begingroup$ We have enough measure theory to do Lebesgue measure. We do not have integrals yet but I bet we will have them within a year. Basic undergraduate level calculus is not really being concentrated on at the moment, but there is no theoretical obstruction -- this is an open source project which people work on in their spare time. All the infrastructure is there for training someone in how to do this stuff in Lean, we just need people to do it. Current developments are very much guided by interests of the group. I like perfectoid spaces, so perfectoid spaces are slowly becoming a reality. $\endgroup$ Sep 22, 2018 at 13:20
10
$\begingroup$

This might be slightly controversial, but I think that one thing that would be valuable to formalize in Lean is the definition of a set.

Working mathematicians are used to formalizing things in terms of sets. Currently, I believe that requiring working mathematicians to swallow type theory before they can even get started with a theorem prover is a significant barrier to entry. It's just a hunch, but I think you'll get more buy-in from the mathematician in the street if you let them work set-theoretically.

Although I know that type-theoretic proof assistants have certain practical advantages, some people, such as John Harrison, have advocated a return to set theory.

$\endgroup$
3
  • $\begingroup$ Lean has a model of ZFC $\endgroup$
    – Kenny Lau
    Sep 26, 2018 at 18:31
  • 2
    $\begingroup$ @KennyLau : Thanks for pointing that out. I suspect, however, that this falls far short of allowing a beginning user of Lean to start formalizing basic definitions and theorems using set-theoretic intuition without having to master type-theoretic ways of thinking. $\endgroup$ Sep 26, 2018 at 18:34
  • 2
    $\begingroup$ Actually, for doing "naive set theory" the type "set A" of subsets of a fixed universe type A behaves much more straightforwardly. But I'm guessing that this isn't what you mean... I am open to any suggestions for how to make set theoretic reasoning more natural inside a proof assistant that is reasonably flexible but ultimately based on DTT. $\endgroup$ Sep 27, 2018 at 2:48
9
$\begingroup$

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.

$\endgroup$
4
  • 2
    $\begingroup$ I feel like we are a million miles away from all of those. $\endgroup$ Sep 21, 2018 at 17:47
  • $\begingroup$ @KevinBuzzard Is (2) really as far away as (1)? (Genuine question, not rhetorical) $\endgroup$
    – Yemon Choi
    Sep 21, 2018 at 21:33
  • $\begingroup$ I am ignorant of the general areas of (1) and (2) and I should take more care before I speak. Yemon come to Zulip and explain the definition to a computer scientist and get their opinion. $\endgroup$ Sep 21, 2018 at 21:46
  • 1
    $\begingroup$ Brownian motion is probably the most accessible of these given current Lean. But there's lots of basic machinery it would be worthwhile doing first. (As an example, I think Stone-Weierstrauss isn't in yet, but probably all the groundwork is there.) $\endgroup$ Sep 22, 2018 at 0:25
7
$\begingroup$

After finite structures, finitely presented groups are the most natural mathematical beings understandable for computers. Many infinite groups have finite presentations and so they can be formalized in any Theorem Prover. Many decision problems in group theory (and low-dimensional topology) can be stated in terms of finitely presented groups (word problem for example). So, f.p groups should be formalized for such programs.

$\endgroup$
2
  • 2
    $\begingroup$ Just as a clarification: Lean is a theorem prover, not a computer algebra system. While finitely presented groups have mathematical interest connecting to their algorithmic content, as well as other uses in pure math, I would caution against the presupposition that finite things are easier to reason with than infinite things. In a theorem prover, difficulty usually scales with difficulty to describe the objects in a pure math setting, so that more abstract is usually better. $\endgroup$ Sep 27, 2018 at 2:55
  • 1
    $\begingroup$ As I understand from the question, it asks about the math objects which most be formally defined in Lean. So, I proposed f.p groups. $\endgroup$
    – Sh.M1972
    Sep 29, 2018 at 7:37
6
$\begingroup$

I would like unsolved problems and conjectures to be formalized. That is to say, the library would provide the statements-to-be-proved and the user would be responsible for filling in the details.

The reason I think this is interesting is because it creates a very simple bar for declaring a theorem proven: make my computer print "yes" when I patch your proof into the definitions provided by the community. If the person-claiming-a-proof were to provide their own definitions, then I have to carefully review them for subtle holes (i.e. I have the problem that they gave me a valid proof that makes the computer say "yes", but did it prove what they claim it proved?).

A good simple case is the Collatz conjecture. One could imagine a person claiming a computer existence proof that there is a cycle beside 4->2->1->4, but upon close investigation it would be realized that the second cycle the proof was describing was (-1) -> (-2) -> (-1) or 0 -> 0 -> 0 because the theorem-to-be-proven was accidentally defined using integers or non-negative naturals instead of the positive naturals.

For more complicated cases, there are often many of these kinds of subtleties. For example, when defining the complexity class BQP, you cannot say that a quantum gate's coefficients are just real numbers. You have to limit the coefficients to computable real numbers. Otherwise you can solve the halting problem by directly encoding the uncomputable answer into one of your coefficients and performing increasingly detailed phase estimation to extract the encoded bits. In fact, you probably want efficiently computable real numbers since otherwise you cap the "difficulty" of any problem to the difficulty of the decoding process.

$\endgroup$
3
  • 3
    $\begingroup$ Here's a minimal formalization of the Collatz conjecture in Lean: def collatz_fn (n : ℕ) : ℕ := if (2 ∣ n) then n / 2 else 3 * n + 1, theorem collatz_conjecture (n : ℕ) : ∃ m, nat.iterate collatz_fn m n = 4 := sorry. Fill in the sorry with a proof and win eternal fame! $\endgroup$
    – j.c.
    Sep 26, 2018 at 20:34
  • 7
    $\begingroup$ The conjecture formalised above is false because n=0 is a natural number in Lean ;-) $\endgroup$ Sep 27, 2018 at 6:50
  • 1
    $\begingroup$ Whoops, I made the very mistake this post warned against! Try this then: theorem collatz_conjecture (n : ℕ) : n > 0 → ∃ m, nat.iterate collatz_fn m n = 4 := sorry $\endgroup$
    – j.c.
    Sep 28, 2018 at 19:04
5
$\begingroup$

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 ).

$\endgroup$
11
  • 5
    $\begingroup$ I don't think religion can be formalized in Lean. $\endgroup$ Sep 21, 2018 at 23:01
  • 3
    $\begingroup$ @YemonChoi Lean is emphatically not playing the constructivity game that many other theorem provers have done, like Coq/Agda/Matita, even if it is using a dependent type theory foundation. I have heard some convincing arguments that advertising that the proof of Feit-Thompson in Coq is constructive is actually harmful for popularizing the result with mainstream mathematicians, since it suggests that this is somehow not quite the statement you expect, or that the proof is avoiding clarity or brevity in favor of some property that no one who isn't a logician cares about. $\endgroup$ Sep 22, 2018 at 8:03
  • 2
    $\begingroup$ I have trouble believing there are really mathematicians so misinformed that they would think that the Coq proof of Feit-Thompson is constructive is an actual minus. $\endgroup$
    – arsmath
    Sep 23, 2018 at 11:53
  • 3
    $\begingroup$ @DimaPasechnik I'm fully aware of constructive mathematics and its advantages, but it's a bit of a silly mark here. We are talking about a finite group; of course there is an algorithm for producing such composition series (just enumerate them all), and there is nothing about saying your proof is constructive that implies that your algorithm is any better than this. Indeed, it may very well be a whole lot worse. $\endgroup$ Sep 23, 2018 at 19:04
  • 4
    $\begingroup$ @arsmath, It might also be the "vegan effect", i.e. if you say you are vegan and I am not I think you are judging me for not being vegan even if this is not the intent. If Feit Thompson is proven constructively, then a classically trained mathematician looking over the proof will feel intimidated to suggest alternate approaches or improvements if they don't know that they have this seal of approval that they don't understand. Perhaps this is caricature, but the downsides of constructive proof are of a sociological nature, not mathematical. $\endgroup$ Sep 23, 2018 at 19:08
5
$\begingroup$

These theorem provers are founded on type theory, and as well with the popularity of homotopy type theory, it would be nice to see some of type theory itself formalized to get a sort of type theory in type theory. Then formalize some of the metatheory of various type theories like normalization, type checking and inhabitation (or the undecidability thereof), and perhaps some categorical logic (which I personally have found a somewhat nebulous subject, and seeing it formalized would be helpful).

$\endgroup$
2
  • 3
    $\begingroup$ People are working very hard on (modularly) formalising dependent type theory itself, in Coq, for instance, and it's not that easy :-) Voevodsky, for instance, was doing this up until he passed away. People are possibly already using Lean for this purpose as well, I can't recall the main references, but Peter Lumsdaine is of the people working on it, as well as Mike Shulman et al. $\endgroup$
    – David Roberts
    Sep 25, 2018 at 5:03
  • $\begingroup$ I've been going through Mike Shulman's notes on categorical logic, and giving fully formal definitions and nice structural characterizations of even non-dependent linear stuff is tricky. Dependent type theory seems very difficult. $\endgroup$ Oct 2, 2018 at 0:18
5
$\begingroup$

I would like to see Jacob Lurie's books and papers formalized, beginning with his book Higher Topos Theory.

$\endgroup$
4
$\begingroup$

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".

$\endgroup$
16
  • 1
    $\begingroup$ One thing which Lean, or at least its libraries, are not good at is playing with axioms. That is, showing what holds in the absence of the axiom of choice, for example. Although there is a mechanism for finding out if a theorem uses a particular axiom, and AC is one of these, it's no help if all the basic theorems in the library assume AC (in particular when Diaconescu is used to prove LEM from AC). So while it's possible to define your category, Hahn-Banach is true from lean's POV, and so it collapses to the usual category. ... $\endgroup$ Sep 22, 2018 at 4:20
  • 2
    $\begingroup$ In particular, even if you don't use AC you wouldn't be able to prove any objects are not isomorphic in one category but isomorphic in the other. That's metamathematics (which is possible, but looks very different from object level reasoning). $\endgroup$ Sep 22, 2018 at 4:22
  • $\begingroup$ @MarioCarneiro Thanks for the clarification. Do you mean to say we can't specify something like ETCS for Ban? I had in mind something written on MSE by Theo Buehler math.stackexchange.com/questions/110438/… which doesn't quite show that HB is needed to demonstrate that $\ell^\infty$ and $L^\infty$ are isomorphic, but in some sense shows that an isomorphism would have to involve existence of an "exotic" functional on $\ell^\infty$. $\endgroup$
    – Yemon Choi
    Sep 22, 2018 at 5:55
  • 1
    $\begingroup$ What you would be able to do in lean is construct this isomorphism. AC is available as a term, a global choice function / Hilbert epsilon, from which you can do these sorts of "exotic constructions" just like any other. To formalize the metamathematical fact that the proof of this requires heavy axioms would be much more difficult since you would have to reflect the whole theory into an internal logic and work there. $\endgroup$ Sep 22, 2018 at 6:43
  • 1
    $\begingroup$ Wait, I'm not sure I understood the ETCS part of the question. I think if you define a term language for constructing functionals (that does not include any choicy constructors), you can probably show that this isomorphism is not in that language, and this proof would be much easier. This is I guess another way to express the "exoticness" of the isomorphism. $\endgroup$ Sep 22, 2018 at 6:46
4
$\begingroup$

I'm not sure how much interest in theorem proving software one can get among the physically inclined, but I would be interested in seeing a formalization of BPS states. They are representations of the supersymmetry algebra (a finite dimensional extension of the Poincare Lie algebra), that have nontrivial odd part in the annihilator. This property makes them robust against small changes in theoretical parameters, and hence good for computing invariants of manifolds (among other things).

They became popular in theoretical physics in the mid 1990s, around the same time as the word "brane", and physicists close to my area of research use them a lot to count black holes and construct infinite dimensional Lie algebras. However, I am not particularly fluent in this language.

Warning: It is quite conceivable that a bare formalized definition won't do anything for us until we find a way to formalize some supersymmetric theories whose BPS states can be identified. However, some toy models are supposed to be "not too bad for mathematicians".

$\endgroup$
3
  • $\begingroup$ So there is a rigorous definition (in ZFC, say) of these objects? [I only ask because the Yang Mills Clay Millenmium problem is probably not formalisable, it does not seem to be a mathematics question in some sense, so I panic whenever someone mentions theoretical physics] $\endgroup$ Sep 23, 2018 at 20:53
  • 1
    $\begingroup$ @KevinBuzzard As far as I can tell, the question I ask is just a little more complicated than working out (a large subclass of) the unitary representations of $\mathbb{R}^{1,3} \rtimes SO_{1,3}(\mathbb{R})$. Therefore, I am fairly confident there is (in principle) a rigorous ZFC definition. On the other hand, the more relevant and far-harder-to-formalize question is: Given a physical theory with Hilbert space $H$, what are the BPS states in $H$? $\endgroup$
    – S. Carnahan
    Sep 24, 2018 at 16:05
  • $\begingroup$ @KevinBuzzard – These incomplete notes by Andy Neitzke give more details on how BPS states are defined from a representation theory point of view. In the setting of Section 1.3, I think the BPS states are the sub-representations $\mathcal{H}^1_{M, Z}$ with $M = |Z|$ (see the opening paragraph of arXiv:0807.4723). Right now, I don't think the notes give a complete, self-contained definition. For example, the odd part $\tilde{\mathfrak{g}}_-$ of the Lie super-algebra doesn't seem to be specified. $\endgroup$
    – Vectornaut
    Oct 2, 2020 at 15:45
4
$\begingroup$

Maybe attack some of these, and get Lean added to the page's prover list:

http://www.cs.ru.nl/~freek/100/

(it says it was last updated a few weeks ago, so it is still maintained).

$\endgroup$
1
  • 6
    $\begingroup$ I am very much in two minds about these kinds of lists. Yes they are some sort of indication of what has been done, but a lot of entries are either "done" or "could be done if someone just sat down and did it" (e.g. construction of transcendental numbers). What I don't see in this list is a lot of modern research level mathematics. In some sense thisis my point. Say I spend 2 days proving that Liouville's number is transcendental. What have I achieved? All the Lean people knew that could be done, all the mathematicians knew it was true. So what? I would rather concentrate on perfectoid spaces. $\endgroup$ Sep 27, 2018 at 6:46
4
$\begingroup$

Sorry for asking a question here but it is too long for a comment. Or maybe if you tell me it's wrong, I'll delete it and I could post it as a regular question in MathOverflow instead.

What is the difference between Lean and for example Coq ?

You write: "No issues with constructivism, the axiom of choice, quotients by equivalence relations, the law of the excluded middle or anything." Fine. Because a proof assistant like Coq is a nightmare for normal mathematician like me. Honestly I tried to learn Coq. I spent four months some years ago to learn the language and to do all basic exercices I found on the Internet. It's really complicated, not intuitive at all, although quite recreational (watching the goals evolving by trying tactics is a little bit like a video game), and useless for mathematics, because restricted to the intuitionistic part mostly. Of course there is the HoTT extension, but I was been told that there were still a lot of non-trivial mathematical problems to put HoTT inside Coq. And I don't think that HoTT can be a good foundations for mathematics. On the contrary, I think that HoTT will be very useful for people studying type theory.

For example, can you implement easily the theory of locally presentable categories in Lean. It's nice to see that you can prove the Yoneda lemma in Lean, but frankly it's quite a very basic lemma. What about the enriched Yoneda lemma for example ?

$\endgroup$
1
  • 5
    $\begingroup$ I think a suitable answer for this question would then be something like "I would like to see enriched categories and locally presentable categories defined in Lean". $\endgroup$
    – S. Carnahan
    Sep 26, 2018 at 7:17
4
$\begingroup$

Formalised definitions of Kuranishi structures, polyfolds, d-manifolds and/or implicit atlas might be useful, along with the associated construction of virtual fundamental class or chain. These are all structures that exist on various moduli spaces of pseudoholomorphic curves in symplectic geometry, and allow us to extract invariants.

I would guess that a proof that these structures actually exist on moduli spaces is probably too hard for most current theorem assistants, but already a formal definition might help to clarify various things: the definitions are extremely subtle, and the experts often exchange lengthy papers which illuminate or query different aspects of the definitions.

You should probably do manifolds first, though, if you haven't already...

$\endgroup$
2
  • 2
    $\begingroup$ Manifolds are absolutely on our hit list and they will surely be done within a year. Where we go after that will depend on who is around I guess. $\endgroup$ Sep 27, 2018 at 6:52
  • 1
    $\begingroup$ Jonny, as you may have guessed if you saw my name in previous comments, this is an important reason why I got interested in proof assistants. I think formalizing the algebraic topology part of Pardon's first VFC paper is doable, and it doesn't even require smooth manifolds. $\endgroup$ Oct 1, 2018 at 8:43
4
$\begingroup$

Why formalize complex objects like topological groups when so much fun can be had with natural, simple objects like undirected graphs? There's also tons of open questions involving these simple beings. Erdös loved them. So I suggest to have a look at simple undirected graphs.

$\endgroup$
4
  • 3
    $\begingroup$ Yes, and then you could check Robertson and Seymour’s work on graph minors. I once heard someone close to them say “if there is a mistake in the proof, who will ever find it” ... $\endgroup$
    – EGME
    Jun 27, 2019 at 19:51
  • 1
    $\begingroup$ de Bruijn said something like the difficulty of formalizing something is directly proportional to its intuitiveness -- more complex objects tend to have been thought about more carefully by mathematicians already. There have been some difficulties making undirected graphs nice to work with in Lean, but they're almost there! $\endgroup$ Oct 16, 2020 at 4:21
  • $\begingroup$ That's interesting @KyleMiller. But I still wonder whether simple, undirected graphs are harder to formalize than, say, Lie groups or Heyting algebras? $\endgroup$ Oct 16, 2020 at 8:09
  • 1
    $\begingroup$ Formalizing the basic definitions of simple undirected graphs is certainly easier, and the design issues come from trying to make the interface support the intuitive ways we think about them. Having it so that subgraphs "are" graphs is still not completely solved for example (there are many solutions, but each has its own set of tradeoffs). But still, it didn't take very long to be able to refer to a simple graph G with a finite vertex set V G and prove ∑ v : V G, degree v = 2 * (edge_finset G).card (that is Lean code for the degree-sum formula). $\endgroup$ Oct 16, 2020 at 18:55
3
$\begingroup$

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.)

$\endgroup$
3
  • 3
    $\begingroup$ I am certainly not an expert on these things, but I think we already have those. There is a formalisation of the Halting Theorem in the math library of Lean. $\endgroup$
    – jmc
    Sep 21, 2018 at 20:35
  • 5
    $\begingroup$ Hah, my work is vindicated! :D Indeed, we have the definition of a Turing machine, as well as computable functions and computable sets. I would like to get more into recursion theory on the one hand, and complexity theory on the other, but all the mathematicians around me think it's not interesting enough. It's too bad we don't have any big names of complexity theory interested in formalized mathematics. (which is a bit ironic since we are doing math on computers and they are doing computers in math) $\endgroup$ Sep 22, 2018 at 4:36
  • 2
    $\begingroup$ Can you do time complexity? I would love to see the Time Hierarchy Theorem formalized (especially since the proof in the most well known textbook is wrong...). $\endgroup$ Sep 22, 2018 at 12:19
3
$\begingroup$

One of the outstanding problems in finite element analysis is how to come up with good sets of basis functions to discretize mixed problems. By mixed problems I mean partial differential equations that can be derived through minimization of some convex functional, but with a constraint. A classic example is the Stokes problem, which describes the flow of very viscous fluids: find a velocity field $u$ in a nice domain $\Omega$ that minimizes the free energy dissipation

$$J(u) = \int_\Omega\left(\mu\nabla u : \nabla u - f\cdot u\right)dx,$$

where $\mu$ is the viscosity and $f$ the body forces on the fluid, with the added constraint of incompressibility:

$$\nabla\cdot u = 0.$$

This can be expressed instead through finding a critical point of the Lagrangian

$$L(u, p) = J(u) - \int_\Omega p\nabla\cdot u\, dx$$

where $p$ is the pressure field. For unconstrained problems, we can triangulate the domain and take the solution $u$ to be a polynomial of pretty much any degree in each triangle and everything converges nicely as you refine the mesh. Constrained problems like Stokes are much harder! The discretization for the velocity and pressure fields have to be carefully chosen in order to get a non-singular finite-dimensional linear system. The most common choice is to take the velocity to be piecewise quadratic and the pressure to be piecewise linear in each triangle; this is called the Taylor-Hood element. But there are many other elements with various tradeoffs.

The proof that a given element pair works -- that it satisfies a discrete Ladyzhenskaya-Babuska-Brezzi condition -- is usually confusing and arduous. It would be cool if these proofs could be formalized. It would be publication-worthy if the techniques used could enable the discovery of new element pairs. More generally, one could try to formalize finite element exterior calculus.

$\endgroup$
2
$\begingroup$

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

https://www.youtube.com/watch?v=6HCz1tFqIcs

$\endgroup$
2
  • 35
    $\begingroup$ Probably a human has to understand it first .... $\endgroup$
    – LSpice
    Sep 21, 2018 at 14:44
  • 10
    $\begingroup$ There are claims in this article quantamagazine.org/… that there are humans who claim to understand it. $\endgroup$ Sep 21, 2018 at 17:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.