Claude Produced a Machine-Checked Proof of Fermat's Last Theorem in 13 Million Lines of Lean

Anthropic published what it describes as the first complete, computer-checked proof of Fermat's Last Theorem, written in the Lean proof assistant by Claude agents over 11 days with limited human intervention. The result is large: roughly 13 million lines of Lean code and 29,500 intermediate theorems, more than five times the size of Mathlib, the community-maintained Lean mathematics library.

The important property is not the size but the checking. Anthropic says the proof uses only Lean's three standard axioms and contains no omitted steps, meaning no placeholder arguments and no additional axioms introduced to close a gap. That claim can be verified mechanically by anyone who runs the Lean kernel against the published repository, which puts it in a different category from a self-reported benchmark score. Kevin Buzzard of Imperial College London, who leads the long-running human effort to formalize the same theorem in Lean, called it an extraordinary autoformalization achievement.

Two limits deserve stating plainly. The underlying mathematics was already proved by Andrew Wiles and Richard Taylor in the 1990s, so this is a translation of an existing argument into machine-checkable form rather than a new theorem. And the human blueprint work that broke the proof into formalizable pieces predates the model. What changed is the speed of a task where correctness can be checked by a machine, which is exactly the setting where long-horizon agents are least likely to produce an undetected error.