Claude Formally Proves Fermat's Last Theorem in 11 Days with 13M Lines of Lean Code

Achievement: First Complete Formal Verification of Fermat's Last Theorem

Anthropic announced that its AI model Claude completed the first full formal verification of Fermat's Last Theorem in 11 days. Formal verification translates mathematical reasoning into a format that a computer proof assistant — here Lean — can check line by line. Human experts had originally estimated the task would require several years.

Fermat's Last Theorem, proposed in 1637, remained unproven until Andrew Wiles published a proof in 1995; that proof took months for peer reviewers to fully confirm. Claude's Lean proof comprises over 13 million lines of code, making it the largest Lean proof to date. It simultaneously proves 29,500 intermediate theorems, covering mathematical areas that had never before been formalized.

Methodology: From Failed Agents to Prove2Me Collaboration Platform

The project was initiated by Anthropic researcher Tianyi Peng. Early attempts saw Claude agents repeatedly lose track of the goal and suffer collaboration breakdowns. The team then switched to Prove2Me, an open‑source collaboration platform designed specifically for mathematical formalization. Prove2Me maintains a theorem dependency graph that allows multiple Claude agents to work in parallel while isolating different modules to prevent context interference. A team of agents completed the entire proof in under two weeks, consuming approximately 6 billion output tokens.

The following image shows key milestones from the Prove2Me plan, illustrating how the proof was decomposed into three core sub‑theorems:

Verification: Zero sorry Statements, Independent Kernel Confirmation

The entire proof relies only on Lean's three standard axioms, with no sorry statements or unverified assumptions. Beyond Lean's built‑in checker, an independent kernel written in Rust called nanoda also performed a full verification, confirming 1,052,234 declarations without error.

Expert Review and Broader Implications

Kevin Buzzard of Imperial College London, who leads a community effort to formalize the same theorem, reviewed the work and commented that this extraordinary automated formalization achievement proves Fermat's Last Theorem without any extra assumptions beyond the mathematical axioms. He added that if automated formalization of FLT is already possible, we have taken a major step toward automated formalization of modern mathematical literature.

The significance extends beyond this single theorem. Formal verification could transform the mathematical peer‑review process. Wiles's proof required months of human checking, and history contains erroneous proofs that persisted for years. As AI begins to produce mathematical proofs at scale, human reviewers will be unable to keep pace without machine‑checked counterparts. Anthropic suggests that future proofs submitted for human review may routinely be accompanied by a formalized version.

Fermat famously scribbled in a margin that he had a marvelous proof too large to fit. Over three centuries later, that "marvelous proof" has become 13 million lines of machine‑verified code — whether Fermat would feel vindicated or offended remains an open question.