Anthropic says Claude produced the first computer-checked proof of Fermat's Last Theorem

Anthropic said on September 4, 2026 that its Claude model produced the first complete, computer-checked formal proof of Fermat's Last Theorem, working largely autonomously over 11 days to encode the proof in the Lean programming language.

What's new

Anthropic's research post states: "We are sharing the first complete computer-checked proof of Fermat's Last Theorem. Claude worked largely autonomously over 11 days to write the proof in the Lean programming language." The effort was led by Tianyi Peng, an Anthropic researcher whose group at Columbia University builds AI-formalization tools, who set out to test whether Claude could make progress on formalizing the theorem — a project that, in Anthropic's words, "went further than he expected."

Over those 11 days, "Claude produced the first end-to-end, computer-checked proof of FLT," writing 13 million lines of Lean and proving 29,500 intermediate theorems along the way. The finished proof was checked by the Lean proof assistant using only its three standard axioms, and an automated comparator confirmed the formalized statement matches the FLT statement already in Mathlib, Lean's community mathematics library.

Anthropic shared the result with Kevin Buzzard, the Imperial College London mathematician who in 2024 kicked off a multi-year community effort to formalize Andrew Wiles's original proof in Lean. Buzzard called it "this extraordinary autoformalization achievement," noting it "proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," and that the work touches "autoformalization of algebra, harmonic analysis, geometry and number theory."

Context

Fermat's Last Theorem — that no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n greater than 2 — was scrawled in a book margin by Pierre de Fermat around 1637 and went unproven for over 350 years. Andrew Wiles finally proved it in 1995 with a 129-page proof that took months of expert work to verify. A decade later, computer scientist Jan Bergstra proposed converting that proof into a form machines can check automatically, and Buzzard's community project has spent multiple years building toward exactly that using Lean.

Anthropic frames this as distinct from other recent AI mathematics headlines, such as AI-assisted work on the Riemann hypothesis that aimed to produce novel results. Here, the novelty is verification, not discovery: taking an already-proven theorem and mechanically checking every logical step the way a calculator checks arithmetic.

Why it matters

Verifying a complex mathematical proof by hand can take years, and history is full of proofs that stood unchallenged before subtle flaws were found. Anthropic argues that if AI systems can reliably formalize proofs at this scale, it could shrink that verification burden significantly — a capability that matters more, not less, as AI systems also start producing new mathematical results of their own that need checking.

The achievement is also a concrete data point on autonomous, long-horizon AI work: 11 days of largely unsupervised effort producing a proof artifact large and coherent enough for outside experts to review and endorse, rather than a short benchmark task. Anthropic says it hopes the result signals a future where formal verification becomes routine enough that trust in the published body of mathematics gets easier to maintain, not harder, as more proofs — human and AI-generated alike — pile up.