Claude autonomously formalizes Fermat's Last Theorem in Lean in 11 days

Anthropic says its AI produced the first end-to-end, computer-checked proof of Fermat’s Last Theorem, a result unproven for over 350 years and first cracked by Andrew Wiles only in 1995. Working largely on its own for 11 days, Claude wrote roughly 13 million lines of code in the Lean proof assistant—more than five times the size of Mathlib, the community proof library it built on—and established some 30,300 intermediate theorems, 29,500 of which fed the final proof. The output was verified by Lean using only its three standard axioms, with a comparator confirming the proven statement matches Mathlib’s own formulation.

The significance here is verification rather than new mathematics. Unlike AI work on the Riemann hypothesis that generated novel results, this effort translates an existing (Darmon–Diamond–Taylor simplification of Wiles’s) proof into a form a machine can check step by step, eliminating the years of human review that complex proofs typically demand. Human involvement was minimal—researcher Tianyi Peng offered only occasional high-level nudges about what to prioritize. Early single-agent attempts stalled as agents lost track of project state; the breakthrough came from Prove2Me, an open collaborative platform that maintains a dependency graph of theorem statements, separates statements from proofs to speed compilation, and lets dozens of agents work in parallel without the memory degradation that sank earlier runs.

The run consumed about six billion output tokens from an internal research model roughly comparable to Claude Fable 5.1, orchestrated through a Claude Code–based multi-agent harness. Imperial College’s Kevin Buzzard, who leads the community FLT formalization effort begun in 2024, called the achievement extraordinary and noted the artifacts are now robust enough to build upon. The broader implication: as AI generates more proofs, cheap automated formalization could make it far easier to trust—and to audit—the foundations of mathematics, a job that has historically taken human reviewers months or years.