Kevin Buzzard

I heard officially yesterday that the EPSRC (the UK science funding body) have awarded me a 5 year research grant to begin the task of formalising a proof of Fermat's Last Theorem in Lean, an interactive theorem prover! The grant starts in October 2024.

I don't know whether the whole thing can be done in 5 years; I will run it as an open source project and a lot will depend on who else decides to get involved. I am confident that the main objective I highlighted in the grant, namely to prove enough to *reduce* the proof to results which were known by the end of the 1980s (i.e. pre-Wiles/Taylor-Wiles), is achievable. But there will be lot of other things which need doing as well, for example I cannot see a way of avoiding the trace formula, and I cannot see a way of avoiding global class field theory, and I cannot see a way of avoiding Mazur's theorem classifying the torsion subgroups of elliptic curves. At the start I will take all of these things as black boxes and concentrate on the R=T stuff. After proving the relevant R=T theorem it will be time to re-assess. Note that it will certainly take a long time to even (a) define R (b) define T (c) define the map from R to T (I'll need it in the Hilbert modular form situation, and Hilbert modular forms have never been formalised in any theorem prover). Note that whilst I will initially be skipping proofs which were known in the 80s, it is not possible to skip *definitions*. And even the definition of an automorphic representation will be challenging to formalise.

But now I have time :-) (or more precisely, in 2024 I'll have time...)

I've been watching @tao@mathstodon.xyz 's approach to running the Polynomial Freiman-Ruzsa formalisation project with interest. This is Terry's second Lean project; the first was essentially a single-author project, and my understanding is that part of the motivation for embarking on the second was that he wanted to see what a collaborative formalisation experience was like. Having been involved in several of these I would definitely say that they're great fun and that you learn a lot both about cool Lean tricks and about mathematics (e.g. from talking to other humans about the material).

Terry's project will probably be completely done in a week or two, which is of course on the face of it extraordinary -- it is adding more and more weight to the claim that top modern research level combinatorics can now in many cases be formalised in real time. See Bhavik Mehta's post https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/ on my blog for more discussion on the topic of formalising modern combinatorics.

One thing I've learnt from the PFR project is a really powerful use of Patrick Massot's blueprint software: Tao has written LaTeX to break proofs down into bite-sized parts, turning a complex proof into a series of simpler lemmas, proved in LaTeX not Lean, all represented as blue nodes in the blueprint graph https://teorth.github.io/pfr/blueprint/dep_graph_document.html . Every couple of days there are updates from Terry on the Lean Zulip (eg here https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.203.2E0/near/404022843 ) about who's doing what, and what is up for grabs. Most blue nodes seem to be done in one or just a few Lean sessions, they are nicely-sized projects.

I think these techniques will work very well for a focussed week-long PhD student workshop based on formalising some of the theories needed for the Fermat proof.

Thanks a lot to Bhavik Mehta, who over the summer completely formalised the breakthrough new Campos-Griffiths-Morris-Sahasrabudheupper upper bounds on Ramsey numbers in Lean, and then wrote a guest post about it for my blog https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/ .

This is nontrivial research level mathematics (which was featured in Quanta, Nature etc) being formalised in real time, something which it wasn't at all clear to me would be possible 6 years ago when I started looking at theorem provers. Right now though, the ability to formalise breakthrough results in some given area depends highly on the area. The London Number Theory Seminar talk last Wednesday was about local-global compatibility in a torsion Langlands correspondence https://researchseminars.org/talk/LNTS/115/ and no theorem prover is remotely near even *stating* the results which were announced in that seminar, let alone proving them. My future work on formalising a proof of Fermat's Last Theorem will hopefully start addressing these matters.

One file to go before the main phase of the port of mathlib from lean 3 to lean 4 is complete!

@andrejbauer@mathstodon.xyz @tao@mathstodon.xyz Only combinatorics. I still maintain that it would be an extremely long project to even *state* the main theorems in any of the recent papers written by Toby Gee or Ana Caraiani, two other number theorists in my department. And proving them would be completely inaccessible -- even proving FLT is a gigantic project and this is from the 90s. There are still lots of problems in the way of making formalisation of all modern mathematics easy.

@ProfKinyon The Lean 4 version of the game had apply ... at which was missing in Lean 3.

All of the function and proposition world thing was to really try and explain that logical implication can be thought of as a function, and all of that was an attempt to make students understand how apply f could turn the target of f into its source and thus argue in a direction which they don't normally think about. In the Lean 4 version I have dumped this completely, there are no abstract propositions at all, it's all numbers, and we can argue the normal way (forwards) with apply at and it's much easier.