Lean at the ICM

Stream: general

[Kevin Buzzard]

So I have been invited to give a plenary lecture at the International Congress of Mathematicians, the conference where they hand out the Fields Medals. The talk takes place in July 2022 and there is also some sort of write-up, which for some reason has to be finished by September 2021, although when my advisor spoke at the ICM he released an "official version" of his talk and also an "expanded version", which was the one everyone read because it was the one on his website.

This gives us a "deadline". Ever since 2017 this community has been achieving bigger and bigger mathematical goals, doing stuff which is not in the other provers (even though sometimes it could have been). One can certainly be optimistic that by July 2022 we will have achieved some sort of approximation to the Scholze challenge -- whether we will have achieved it might depend on the small print, but for sure Johan and the team will have achieved something which will be easy to sell.

Thinking of other big projects, there are two very natural ones which could be in really good shape by July 2022. Note that I am not too worried about whether it's Lean 3 or Lean 4, the audience will not know the difference.

1) Sphere eversion.

What we have learnt from experience is that a successful non-trivial formalisation project seems to benefit from the following:

*) A blueprint -- a careful mathematical explanation of what is going on
*) A mathematical leader/leaders -- someone who knows all the maths, can deal with questions arising from the blueprint.
*) A formalisation leader/leaders -- someone who is constantly thinking "what is the next thing that can be achieved, and who is going to do it" -- and if they don't know anyone working on it, they may well start on it themselves.

For sphere eversion we have a mathematical leader in Patrick, and a beautiful online blueprint also made by Patrick. But Patrick has not yet had the time to be a formalisation leader, he is busy with other things (like writing Lean courses for undergraduates and literate tactics). If we can find a formalisation leader, this project could be in really good shape by July 2022. Note that you do not have to know all the mathematics back to front to start to do this job -- Johan has been the formalisation leader for the LTE and he learnt the mathematics (i.e. read the relevant part of Scholze's document extremely carefully) whilst figuring out how to lead, i.e. working out which bits could be broken off as individual files with sorries in which other people could work on.

2) Formalising algebraic geometry.

This is a more open-ended goal, and there are several things one can target.

Firstly I think a flagship definition would be the etale cohomology of schemes. On paper this looks highly feasible. Bhavik has developed a very general theory of sheaves on sites, and Scott might well have made the crucial breakthrough with a definition of a derived functor. The definition and basic properties of etale morphisms of rings should be easily do-able, because Lean seems to be very strong at this kind of commutative algebra, we already have a plethora of results at this kind of level. Whether this translates into a definition and basic properties of etale morphisms of schemes is not something that we, or anyone in the formal verification community, know yet. But if it does then this will be all we need.

Another thing we could do is projective schemes/morphisms; I have been thinking about graded rings for weeks now, and will start making PR's this week.

Note that the computer scientists are always keen on theorems to go with definitions, but nontrivial theorems might well be over a year away.

However there is something else which one can think about here, which is Lean integration with the Stacks Project. This is something which everyone seems to be keen on, but again never seems to happen, mostly because I'm the most enthusiastic one at this end and I don't know what a yaml file is so never quite know where to start.

3) Other stuff.
Are there any other projects which we think might look impressive to mathematicians and could well be in good shape within 13 months? Once we have group cohomology (now on the horizon) we can get to Galois cohomology and hence state the main theorems of class field theory, but proving them will be a long way away. A student on my PhD program, Jamie Bell, has formalised the statement of BSD in Lean -- he sorries plenty of Props but no data (and there is a slip in that file, a typo in the definition of doubling which we only discovered when filling in sorries, so let that be a warning about this approach, as if we needed one. Perhaps the reason that the mathematicians are far less fussed about this sort of thing than the computer scientists is that we are so used to dealing with typos in LaTeX documents :-) ). Hales was talking about formalising the Clay problems this way back in 2017. I think that an ICM audience might be interested to hear about progress in this area.

[Johan Commelin]

Congratulations! This is really cool!

[Oliver Nash]

I wonder if we have a lean-gptf PR that is non-trivial enough to suggest the promised land? If there exists a PR where it golfed a proof in some way that was surprising to a mathematician, it might just be worth mentioning.

[Riccardo Brasca]

Congratulations!!

[Yaël Dillies]

That's great! How could a Cambridge second year undergraduate fit in such a project?
On my part, I am expecting Szemerédi's Theorem to be a much bigger project than what can fit in a summer, but I lack knowledge of the proofs to compare its size to the other projects.

[Kevin Buzzard]

My impression with Szemerédi is that you should spend July working on it with Bhavik and by that time you will have a very clear idea about what is feasible and what is not, and we can go from there.

[Sebastien Gouezel]

Which proof of Szemeredi are you going to consider? I have a L3 student from ENS Lyon doing an internship with me currently, on the ergodic theory proof by Furstenberg, so if this is the proof you are going to look at I could put you in touch!

[Mauricio Collares]

If you are doing the regularity proof I will try my best to help! I haven't got a lot of experience with Lean but a project would be great for that.

[Yaël Dillies]

Oh! I didn't know other people were working on Szemerédi as well! We will follow either of Gowers' proofs. I am leaning towards the hypergraph proof because it is a proper generalisation. As a starter, I'm proving the usual regularity lemma on the szemeredi branch (https://github.com/leanprover-community/mathlib/blob/szemeredi/src/combinatorics/szemeredi/regularity.lean).
So yeah I'm not doing Furstenberg's ergodic proof but Sébastien feel free to put us in touch either way :smile: (I might actually start talking about Lean in French! What a crazy thought)
And Mauricio that would be nice for you to help! But of course, I'm not obliging you in doing my internship :stuck_out_tongue_wink:. When do you have time? We will really start only by the end of June.

[Mauricio Collares]

End of June sounds great! I have a big deadline on June 18th so I'll have more free time after that. Really like the idea of doing Gowers' hypergraph proof too

[Bhavik Mehta]

Yael and I did discuss the other approaches to Szemeredi's theorem, and we decided against formalising Furstenberg's one since it would involve formalising a good amount of measure theory and ergodic theory (and also involve Yael learning such)

[Sebastien Gouezel]

I agree with you: there are too many prerequisites in ergodic theory for Furstenberg's proof, so going the Gowers way is a better idea for formalization (for now :-)

[Patrick Massot]

Kevin Buzzard said:

Note that I am not too worried about whether it's Lean 3 or Lean 4, the audience will not know the difference.

I think Kevin is right that we don't need the big projects to be in Lean 4 before his talk. But hopefully we'll see a massive surge of interested people after his talk, and we really really don't want to be stuck in the middle of the Lean 4 transition at that time. We need a fully ported and documented mathlib4 before July 2022. We won't get another opportunity like this (unless the AI people really do what they promise).

[Mario Carneiro]

We need a fully ported and documented mathlib4 before July 2022.

This is a good goal, but to be perfectly frank I think it is setting expectations too high, and might put too much pressure on the lean 4 team.

[Patrick Massot]

And I also agree with Kevin that we can definitely get the sphere eversion project done before then. Right now it's not moving at all because I prioritized contributing to the liquid tensor experiment. But there is no reason why it couldn't move. If we put a tenth of the energy that went into the liquid tensor experiment into sphere eversion it will be done in a couple of month.

[Patrick Massot]

I don't want to put any pressure on the Lean 4 team. Only on us when we'll have to do manual porting.

[Patrick Massot]

Mario, this is 2022, not 2021.

[Mario Carneiro]

Yes I know

[Patrick Massot]

It's dinner time, but I'd be curious to read more about why you think July 2022 is too optimistic, so don't hesitate to continue writing while I'm away.

[Mario Carneiro]

Porting mathlib in ~1 year implies that lean 4 is usable for mathlib by the end of that time, so it does put pressure on lean 4 (indirectly, by us when some issue in lean 4 prevents us from porting something)

[Mario Carneiro]

It's what I would call a stretch goal. It's possible, but requires a lot of concerted effort from all quarters. We will know much better how feasible this is at the end of the summer, since that's when most of the porting setup work should take place. We need to be ready to systematically port a file by the end of that period, and bring in an army of volunteers to actually do the work, and have documentation for them to follow

[Anthony Bordg]

@Kevin Buzzard Congratulations!

[Amaury Hayat]

I missed this information, but many congratulations Kevin Buzzard ! This is amazing :) In addition, the perspective of hearing about Lean during a plenary talk of the ICM is really exciting !