Claude completes first fully machine-checkable formal proof of Fermat's Last Theorem

Anthropic has announced that Claude completed the first end-to-end, fully computer-checkable proof of Fermat's Last Theorem, translating a proof readable by human mathematicians into formal code a computer can verify line by line, with no "obvious here" steps allowed. After more than 350 years, one of mathematics' most famous results now exists in fully machine-verifiable form.

Formalization means writing every definition, theorem, and inference step in a language the Lean proof assistant can check, so each derivation is verified as legally following from axioms and earlier theorems. Papers written for humans can hand-wave with "it obviously follows," but a formal proof permits no skipped steps. The resulting Lean code reportedly spans roughly 13 million lines.

Fermat's Last Theorem resisted generations of mathematicians — Euler, Legendre, Kummer and others — after Fermat posed it in the 17th century, until Andrew Wiles and Richard Taylor completed the proof in 1994. Moving that proof into a computer-checkable system is another enormous undertaking: in 2024, Kevin Buzzard and colleagues at Imperial College launched a multi-year community project to formalize the theorem in Lean, and the blueprint for just the first phase ran 86 pages.

The Anthropic effort was led by Tianyi Peng, a Tsinghua Yao Class alumnus who graduated in 2017, earned his MIT PhD in 2023, and is now an assistant professor at Columbia University and a researcher at Anthropic, with a long-standing focus on reinforcement learning, AI agents, and formal tools. The project divided work among specialized agents: some filled in mathematical definitions, others attacked intermediate lemmas, some extended existing results toward higher-level theorems, and dedicated agents reassembled the pieces into the complete proof.

Collaboration was not smooth at first. Anthropic said early agents quickly scored some results, but as the project grew they lost track of its overall state and struggled to cooperate effectively. Peng and his Columbia collaborators built a coordination system specifically for mathematical formalization: a shared graph showed which theorems were proven, which prerequisites were missing, and which node to attack next, while the platform kept statements and proofs separate, accelerated Lean compilation, and retained natural-language descriptions of each theorem so agents could search and reuse prior results.

According to the report, Anthropic's final setup was Prove2Me+, a multi-agent harness built on Claude Code. The project consumed roughly 6 billion output tokens in total, and the internal general-purpose research model used was roughly equivalent to Claude Fable 5.1 in capability. Anthropic also said the completed proof relies on only three standard Lean axioms, and the company ran comparison programs to confirm that the theorem statement Claude proved matches the statement of Fermat's Last Theorem in Mathlib exactly.

Humans receded into occasional high-level direction: Peng only sometimes offered guidance such as which directions to prioritize or which theorems to push forward quickly.

Formalization has long been one of the slowest, most labor-intensive corners of mathematics. When a mathematical result of this scale and complexity can be carried into a formal system by AI, the formalization of mathematical literature — long dependent on slow, painstaking human labor — may for the first time be poised for large-scale acceleration. The question to watch is whether this multi-agent formalization pipeline can be reused for other major theorems and for reliability-critical verification in software and safety work.