Fermat’s Last Theorem now has a complete computer-checked proof

Andrew Wiles proved Fermat’s Last Theorem in 1995. The new achievement is an end-to-end formalization: every logical step can be checked by software.

Anthropic reports 13 million lines of Lean, with 29,500 intermediate theorems used in the final proof. The work follows an exposition of Wiles’s argument and incorporates existing community projects and Mathlib. Kevin Buzzard reviewed the result.

Early attempts lost track of the project and failed to coordinate. Progress improved with Prove2Me, which maintained a graph of theorems and their dependencies, helped agents find reusable results, and reduced compilation overhead. The successful run consumed roughly six billion output tokens.

Lean checked the proof, and a separate comparator checked that its final statement matched Mathlib’s statement of the theorem. That last detail matters: impeccable reasoning about the wrong proposition would not establish the result.

The published code provides a concrete artifact to inspect. The next challenge is making these enormous formalizations easier for people to understand and build upon.