The Fermat's Last Theorem project

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

The Fermat's Last Theorem project is a multi-author, open-source effort, led by Kevin Buzzard at Imperial College London, to formalise in Lean a proof of Fermat's Last Theorem. This page describes its aims, its method and its state as of October 2026, including the separate, machine-written formalisation of the theorem announced in September 2026.

The theorem and the proof

Fermat's Last Theorem says that if $x,y,z,n$ are positive integers and $n\ge 3$, then $x^n+y^n$ never equals $z^n$. Fermat raised it in 1637; Andrew Wiles, assisted by Richard Taylor, settled it more than 350 years later. Although the statement is about counting numbers, every known proof uses much deeper mathematics: elliptic curves, modular forms, finite flat group schemes and Galois representations, among other things. Written out in full from the axioms, any known proof would run to several thousand pages.

Aims

The project is funded by a fellowship from the Engineering and Physical Sciences Research Council, "Formalising Fermat" (EP/Y022904/1), worth £934,043, which runs from October 2024 to September 2029. Buzzard announced it on the Lean community's blog in April 2024.

The first goal is not the whole theorem. It is to reduce Fermat's Last Theorem to claims that mathematicians knew by the end of the 1980s, which would then be assumed rather than proved. The grant's own summary puts the same aim another way: to formalise much of the mathematics of a modern proof, and so to reduce the task to formalising results from the 1980s.

Buzzard gave several reasons for the work. Many standard objects of modern number theory had not been defined in Lean or in any other theorem prover, so many recent results could not even be stated, let alone proved; the project would have to define them. Foundational material would go into Mathlib, Lean's mathematical library. And when he wrote, in December 2023, Fermat's Last Theorem was the one problem left unformalised on Freek Wiedijk's list of 100 challenge theorems for computer formalisation.

Method

The proof being formalised is not Wiles's original. It is a modern variant of the Wiles and Taylor–Wiles argument that borrows heavily from the ideas of Khare and Wintenberger, and its route was planned almost entirely by Richard Taylor in discussions with Buzzard. At its heart is still the idea, proved by Wiles in crucial cases, that a certain deformation ring $R$ is isomorphic to a Hecke algebra $T$.

The project is organised with a blueprint, the LaTeX map of the proof whose dependency graph shows which pieces are done, a method described on the polynomial Freiman–Ruzsa conjecture. It works from both ends at once: down from the main theorem, stating the large claims to be assumed, and up from the basics, adding general material to Mathlib, with the aim of meeting in the middle.

Formalisation checks the literature as well as the proof. In 2024 the work on divided powers, on which the theory of crystalline cohomology relies, met a problem in the literature: a lemma in a 1965 paper by Norbert Roby appeared to be false, and the gap blocked a definition the project needed. Antoine Chambert-Loir and María Inés de Frutos-Fernández were formalising the theory; Chambert-Loir worked on a repair, and by December 2024 Buzzard reported the issues sorted out and the project back on track. In the same period Andrew Yang proved in Lean an abstract result of commutative algebra on which the $R=T$ step depends.

In 2026 Buzzard gave a lecture course of eleven lectures on the proof's route, and announced a workshop in London for July 2026, funded by the company Logos Research, to find out which parts of the proof AI tools could formalise. In May 2026 he judged that such tools could not yet reliably formalise definitions correctly, or state theorems in the idiom of Mathlib, without help.

A complete formal proof by other means

On 4 September 2026 Anthropic announced a complete formal proof of Fermat's Last Theorem in Lean, produced, by its account, in about 11 days by dozens of instances of its model Claude working largely on their own on Prove2Me, a collaborative formalisation platform from Columbia University. The proof follows the 1995 exposition of Wiles's argument by Henri Darmon, Fred Diamond and Richard Taylor. It is about 13 million lines of Lean, proves some 30,300 theorems of which about 29,500 are used in the final proof, rests only on Lean's three standard axioms, and adapts pieces of the Imperial project and of an earlier formalisation of the theorem for regular primes. A comparison tool confirmed that the statement proved matches Mathlib's own statement of Fermat's Last Theorem.

Buzzard compiled the code and ran the comparison himself, and reported that it checks out; he also described the proof as gigantic, over 13.4 million lines that take nearly twenty times as long to compile as Mathlib. He noted that the formalisation follows the early literature and adds nothing new mathematically, and that it closes Wiedijk's list. Its route is the older one, not the modern proof the Imperial project follows. In answer to readers who asked whether the program could have exploited a flaw in Lean, he described asking an AI agent to list everything in the code that was neither a definition nor a proof, and inspecting the roughly 100 lines it found, which he concluded only defined a convenience tactic; he added that this was not a perfect approach. What the Lean kernel's check does and does not establish is the subject of What has to be trusted.

State as of October 2026

The machine-written proof goes further than the grant's first goal, since it proves the whole theorem rather than reducing it to the 1980s. Buzzard wrote that it does not discharge the project's other commitments: to add the fundamental objects of modern number theory to Mathlib, which is continuing, and to produce a document through which people can explore the modern proof. The project page still describes the work as ongoing, led by Buzzard and funded until September 2029.

Next

• The equational theories project, a collaboration on a different scale.
• Machine learning and theorem proving, for machine-written proofs in general.