09-05-2026, 12:09 PM
Formalizing Fermat’s Last Theorem — Anthropic, September 4, 2026
Anthropic reports what it describes as the first complete computer-checked formal proof of Fermat’s Last Theorem (FLT). The theorem states that there are no positive integers $a,b,c$ satisfying
$a^n+b^n=c^n$
for any integer $n>2$. Andrew Wiles, later working with Richard Taylor, proved FLT in the 1990s using deep results connecting elliptic curves and modular forms. Anthropic’s achievement is not a new mathematical proof of FLT, but a formalization of the existing mathematical argument in the Lean proof assistant, where every logical step can be checked mechanically. According to Anthropic, Claude worked largely autonomously for 11 days, generated about 13 million lines of Lean code, and proved roughly 30,300 intermediate theorems.
The project used a multi-agent system together with Prove2Me, a collaborative formalization platform that organizes mathematical dependencies as a directed acyclic graph. Different Claude agents could therefore work simultaneously on algebra, number theory, geometry, harmonic analysis, and other components of the proof. The final argument follows a streamlined exposition of Wiles’s proof by Henri Darmon, Fred Diamond and Richard Taylor. The finished proof was compiled and verified by Lean, demonstrating that a modern AI system can formalize mathematics at a scale that previously required enormous amounts of specialized human effort.
The broader significance may extend well beyond Fermat’s Last Theorem. Formalizing advanced mathematics is difficult because proof assistants require every intermediate logical step that ordinary mathematical writing often leaves implicit. AI systems could substantially reduce this burden, making it practical for research papers to be accompanied by machine-verifiable proofs. This could help detect subtle errors in existing mathematics and provide an increasingly important mechanism for checking mathematical arguments generated by AI itself. Formal verification, however, should complement rather than replace clear, human-readable mathematical proofs.
Key takeaways
ARTICLE
Anthropic reports what it describes as the first complete computer-checked formal proof of Fermat’s Last Theorem (FLT). The theorem states that there are no positive integers $a,b,c$ satisfying
$a^n+b^n=c^n$
for any integer $n>2$. Andrew Wiles, later working with Richard Taylor, proved FLT in the 1990s using deep results connecting elliptic curves and modular forms. Anthropic’s achievement is not a new mathematical proof of FLT, but a formalization of the existing mathematical argument in the Lean proof assistant, where every logical step can be checked mechanically. According to Anthropic, Claude worked largely autonomously for 11 days, generated about 13 million lines of Lean code, and proved roughly 30,300 intermediate theorems.
The project used a multi-agent system together with Prove2Me, a collaborative formalization platform that organizes mathematical dependencies as a directed acyclic graph. Different Claude agents could therefore work simultaneously on algebra, number theory, geometry, harmonic analysis, and other components of the proof. The final argument follows a streamlined exposition of Wiles’s proof by Henri Darmon, Fred Diamond and Richard Taylor. The finished proof was compiled and verified by Lean, demonstrating that a modern AI system can formalize mathematics at a scale that previously required enormous amounts of specialized human effort.
The broader significance may extend well beyond Fermat’s Last Theorem. Formalizing advanced mathematics is difficult because proof assistants require every intermediate logical step that ordinary mathematical writing often leaves implicit. AI systems could substantially reduce this burden, making it practical for research papers to be accompanied by machine-verifiable proofs. This could help detect subtle errors in existing mathematics and provide an increasingly important mechanism for checking mathematical arguments generated by AI itself. Formal verification, however, should complement rather than replace clear, human-readable mathematical proofs.
Key takeaways
- Claude did not discover a new proof of FLT; it formalized an existing proof so that Lean could verify it mechanically.
- Fermat’s Last Theorem states that $a^n+b^n=c^n$ has no positive integer solutions when $n>2$.
- The project involved about 13 million lines of Lean code and roughly 30,300 proved intermediate theorems.
- The major breakthrough is in AI-assisted mathematical formalization and verification, potentially making machine-checked research mathematics much more practical.
ARTICLE
┌────────────────────────────────┐
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘