Elektrine lite

← Feed

@xenaproject@mathstodon.xyz

Post #1366386

2023-10-03 10:16 UTC

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

Replies (6)