← Back to feed

Anthropic has published what it calls the first complete computer-checked proof of Fermat’s Last Theorem, produced by Claude working largely autonomously over 11 days.

The work was led by Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization. Peng set out to test whether Claude could make meaningful progress on formalizing FLT — a project the mathematical community expected to take years. The result went further than he anticipated.

The Numbers

• 11 days from start to verified completion (August 6–17, 2026)
• 13 million lines of Lean 4 code generated
• 29,500 intermediate theorems proved along the way
• 5x the size of Mathlib, the principal community library of formalized mathematics

Claude’s proof follows a simplified version of the Wiles proof from Darmon, Diamond and Taylor. Dozens of Claude agents collaborated in parallel: defining concepts, proving intermediate theorems, and using those results to prove progressively harder statements. Human input from Peng was limited to occasional high-level steering — “Jacobian as a scheme sounds high priority,” “push Mazur to be done soon.”

The system crossed the finish line at 02:00:57 UTC on August 18. A Claude agent’s own thinking log captured the moment: ”🏁🏁🏁 The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.”

What Formalization Is (and Is Not)

This is verification, not discovery. Wiles published the original proof in 1995 after a 358-year search that culminated in a 129-page paper and over a year of gap-patching. The community-led Lean formalization project, kicked off by Kevin Buzzard at Imperial College London in 2024, aimed to encode that proof so a computer could check every logical step from first axioms.

The difficulty is scale and granularity. Human proofs skip steps considered obvious. Lean needs all of them. The project blueprint alone runs 86 pages.

Claude’s contribution is completing that encoding. Kevin Buzzard’s assessment: “This extraordinary autoformalization achievement proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon.”

Why It Matters for Mathematics

The practical value is not the FLT result itself — that has been known since 1995. It is the precedent for what AI-assisted formalization can now do at scale.

As mathematical output from AI systems grows, so does the problem of verification. Human review of novel proofs can take months or years. A formalized proof is machine-verifiable in seconds. If Claude-class systems can consistently formalize complex results, the bottleneck on trusting new mathematics shifts considerably.

Early multi-agent runs failed: agents lost track of project state and stopped collaborating effectively. Failed attempts contributed roughly 7% of non-boilerplate code in the final proof — a signal that the approach required significant scaffolding work before it could sustain 11 days of autonomous operation.

The proof and Lean source code are published at github.com/anthropics/fermats-last-theorem.