On September 4, 2026, Anthropic announced that Claude had produced the first fully computer-verified formalization of Fermat's Last Theorem in the Lean proof assistant — a result that took the AI just 11 days of wall-clock time and generated over 13 million lines of code.
What Happened
Fermat's Last Theorem — that no three positive integers can satisfy xⁿ + yⁿ = zⁿ for any integer n greater than 2 — was famously conjectured by Pierre de Fermat in 1637. Andrew Wiles published a proof in 1995 after more than seven years of work. But producing a formal proof, one verified line-by-line by a computer using only logical axioms, remained an open challenge. Human mathematicians estimated such a formalization would take decades.
Claude completed it in under two weeks.
The run, described in detail in Anthropic's technical report, used several dozen parallel agents generating roughly six billion output tokens total. Claude proved 30,300 sub-theorems, of which 29,500 were used in the final proof. The resulting Lean file is the largest formal proof ever constructed in that language.
A Key Assist From an Open-Source Tool
The first formalization attempt failed. Mid-run, Anthropic's team integrated Prove2Me, an open-source theorem-proving scaffold from Columbia University, and completion became possible. This detail matters: the achievement is not purely autonomous AI — it is AI plus open-source tooling plus human engineering decisions made during the run.
The distinction is important because Anthropic has been careful to clarify that Claude did not discover the proof. It translated and formalized Wiles's existing work. As one AI commentator put it, "Fermat's Last Theorem Formalized: Anthropic Completes Full Verified Proof… It Did Not Discover the Proof."
Why It Matters
Lean verified the result using only its three standard axioms. That means the proof is not just a plausible argument — it is mechanically certain.
Imperial College mathematician Kevin Buzzard, who has spent years pushing for formal verification of modern mathematics, called it an "extraordinary autoformalization achievement" and said it "points toward automatic formalization of modern mathematics." The path from human-language proof to machine-checked certainty — which previously required years of specialized effort — may now take days.
The implications extend beyond pure mathematics. Formal verification is used in chip design, cryptography, and safety-critical software. If AI can automate the hard work of writing formal proofs, the cost of building verifiably-correct systems drops dramatically.
What Comes Next
Anthropic has not announced what it plans to formalize next. But with 13 million lines of Lean code now standing as a proof of concept — in the most literal sense — it is hard to imagine the answer to that question staying quiet for long.