Which proof is being formalised?

At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof, although we are currently actively working on fixing this.

From 2024 to 2029 we will be beginning to build a proof of FLT, following a strategy basically due to Khare, and modified by Taylor, taking into account Buzzard's comments on what would be easy or hard to do in Lean. Our strategy uses refinements of the original Taylor–Wiles method by Diamond/Fujiwara, Khare–Wintenberger, Skinner–Wiles, Kisin, Taylor and others – one could call it a 21st century proof of the theorem. During this initial phase of the project, we shall also be assuming many nontrivial theorems without proof, as long as they were published by 31st December 1989. To get technical for just a second – we shall for example be assuming the existence of Galois representations attached to weight 2 Hilbert modular forms, we will assume Langlands' cyclic base change theorem for \(\operatorname{GL}_2\), Mazur's theorem bounding the torsion subgroup of an elliptic curve over the rationals, and several other nontrivial results which were known by the end of the 1980s.

The upshot of this is that, by 2029 at the end of this first phase, the project should contain a complete proof that FLT follows from results that were known to humanity in the 1980s. In particular, one naive way of understanding the goal is that it is a “formalization of the papers of Wiles and Taylor–Wiles, assuming the results in the references of those papers”. However, as noted above, we will actually be taking a slightly different path.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.