Fermat's Last Theorem in Lean 4

[mklabgr]

Anthropic’s Fermat’s Last Theorem project is a large formalization of Fermat’s Last Theorem in Lean 4. It encodes the modern proof developed through the work of Frey, Serre, Ribet, Wiles, and Taylor–Wiles, showing formally that for integers $n \ge 3$ and positive natural numbers $a,b,c$, the equation $a^n+b^n=c^n$ has no solutions. The repository contains more than 60,000 Lean modules and nearly 30,000 formally stated theorems, together with an offline HTML interface for exploring the proof and its dependencies. Much of the Lean code was produced by AI agents building on existing human-written formal mathematics from projects such as Mathlib and the Imperial College London FLT project.

The significance of the project is not that it introduces a new proof of Fermat’s Last Theorem, but that it makes the established proof machine-checkable at a very deep level. Anthropic reports verifying the result through a complete Lean build, the Lean comparator tool, and nanoda, an independently implemented Lean kernel written in Rust. The final theorem uses only Lean’s standard axioms and contains no unfinished proofs or unsafe shortcuts. The project therefore serves as an important demonstration of how AI can assist with the formalization of extremely advanced mathematics while leaving the Lean kernel responsible for checking the logical correctness of every step.


PROJECT