Core Announcement: AI Completes Formal Proof of Fermat’s Last Theorem
Anthropic announced on September 5, 2026, that its Claude system completed the first end-to-end, computer-verifiable formal proof of Fermat’s Last Theorem. Key facts:
- Release date: September 5, 2026
- Completion time: 11 days
- Model used: Anthropic’s internal general-purpose research model (capability roughly equivalent to Claude Fable 5.1)
- Code output: approximately 13 million lines of Lean code
- Theorems generated: about 30,300 computer-verifiable theorems, 29,500 incorporated into the final proof
- Scale comparison: exceeds Lean’s core library Mathlib by over 5×, making it the largest Lean proof project to date
- Verification status: passed all Lean checks using only three basic standard axioms
Led by Tianyi Peng, an Anthropic researcher and清华姚班 alumnus now serving as Assistant Professor at Columbia Business School and MIT PhD.
The Formalization Challenge: Turning Human Proofs into Machine-Checkable Code
Fermat’s Last Theorem, proposed by 17th-century mathematician Pierre de Fermat, states that the equation aⁿ+bⁿ=cⁿ has no positive integer solutions when n>2. The conjecture remained unsolved for 358 years until Andrew Wiles announced a proof in 1993, with a critical gap patched with Richard Taylor’s help in 1994–1995. The published proof spans 129 pages.
The key counterpoint: numbers, logic, and definitions considered “obvious” to professional mathematicians are omitted from human-written papers—yet Lean’s verifier has no such common-sense shortcuts. Every step, definition, and intermediate conclusion must be explicitly encoded. This is the essence of mathematical formalization: converting natural-language proofs into machine-checkable programs.
Kevin Buzzard of Imperial College London initiated the大型开源 project in 2024 to formalize Wiles’ proof in Lean, expected to take years. AI has now accelerated this timeline dramatically.
Multi-Agent Collaboration and the Prove2Me Platform
The effort required dozens of parallel Claude Agents, consuming approximately 6 billion output tokens.
Initial attempts failed due to coordination issues—agents quickly lost track of the overall progress. The breakthrough came with Peng’s team-developed Prove2Me collaboration platform, which decomposes large proofs into a directed acyclic graph (DAG). Top-level objectives (e.g., proving Fermat’s Last Theorem) are recursively broken into smaller sub-theorems, enabling agents to specialize in definitions, lemma proofs, or upward approximation.
Final outcomes:
- ~30,300 theorems verified by Lean
- 29,500 theorems integrated into the final proof chain
- ~13 million lines of Lean code
- Scale exceeds Mathlib by 5×+, setting a new benchmark for formal mathematics
Additional validation confirmed the mathematical命题 matches Mathlib’s formal definition exactly.
Target Users and Strategic Recommendations
- Ready for adoption: Research teams working on automated theorem proving, formal verification, or mathematical logic—can adopt Prove2Me’s DAG task-decomposition approach
- Collaboration opportunities: Lean/Mathlib open-source communities and formal mathematics labs—consider integrating this platform for mid-scale proof engineering
- Wait and observe: Researchers seeking elegant, concise proofs—the 13 million lines include redundancy, and the community is already exploring subsequent code-compression efforts
Final Thoughts
Claude did not discover an alternative proof or replace Wiles’ work. Its true significance lies in scaling a complex, cross-domain proof工程 to automation for the first time, transforming formalization from a multi-year manual endeavor into an engineering-grade research infrastructure. AI’s role in mathematics is evolving from problem-solving to knowledge synthesis and verification automation.