Anthropic’s Claude autonomously formalizes Fermat’s Last Theorem in Lean over 11-day campaign
Translating Sir Andrew Wiles's legendary 1995 proof into machine-verifiable code, Claude proved 29,500 intermediate theorems strictly using Lean's standard axioms.
Original cover art, generated for this story. THE VISSION does not republish third-party press imagery.
- Anthropic has achieved the first complete, computer-checked formalization of Fermat's Last Theorem, translated into Lean by Claude over an 11-day run.
- The resulting proof spans 13 million lines of Lean code—five times the size of Lean's principal math library, Mathlib—proving 29,500 intermediate theorems.
- Claude agents were coordinated via Prove2Me, an open collaborative platform maintaining a directed acyclic graph of theorems to distribute mathematical tasks.
- The verified proof contains no unproved placeholders or 'sorry' tags, establishing a new milestone for AI's capacity to assist in high-level research mathematics.
Anthropic has announced that Claude has successfully completed the first autonomous, computer-checked formalization of Fermat’s Last Theorem (FLT), marking a monumental milestone in automated reasoning and research mathematics, according to official company releases and technical documentation. Over a concentrated 11-day campaign, Claude translated the complex algebraic geometry and modularity reasoning of Sir Andrew Wiles's legendary 1995 proof into the Lean programming language, allowing a computer to verify every single logical step of the proof.
The scale of the formalization is exceptionally large in the field of computer-assisted mathematics. Claude produced 13 million lines of Lean code—over five times the size of Lean's principal community library, Mathlib—and proved 29,500 intermediate theorems along the way. Wiles's original proof, while a masterpiece of human mathematics, spanned over 100 pages and took months for human peers to verify. Autoformalization at this scale was previously expected by the research community to take several years of intensive, human-led effort.
The breakthrough was enabled by a specialized multi-agent architecture built on Prove2Me, an open collaborative platform designed by Anthropic researcher Tianyi Peng and collaborators at Columbia University. Prove2Me coordinated a swarm of Claude agents by maintaining a directed acyclic graph (DAG) of theorem statements. This scaffolding allowed mathematical sub-agents to claim open conjectures, draft Lean proofs, and submit them to validation sub-agents. This structural isolation prevented individual agents from getting bogged down in circular logic or state decay over the 11-day run.
Importantly, the finished formalization was fully checked and accepted by the Lean proof assistant, relying strictly on Lean's three standard axioms. The repository contains zero unproved 'sorry' tags—the standard placeholder in Lean for unproven logical steps—confirming that the entire mathematical cascade is sound. Anthropic stated that the project builds upon previous open-source formalization efforts, including the Imperial College London FLT project led by Kevin Buzzard and the flt-regular project, and has released the full proof on GitHub for public inspection.
Formalizing Fermat's Last Theorem represents a shift from AI as an autocomplete tool to AI as a rigorous scientific researcher. By translating high-level, human-written mathematics into computer-verifiable code, Claude has demonstrated that 'autoformalization' can scale to the most complex proofs in human history. This capability provides a concrete blueprint for using proof assistants to rigorously verify AI-generated mathematics, establishing a crucial safety and verification loop that bypasses the high cost and latency of human review.