Has Fermat's Last Theorem been formally proved in Lean?

Yes. On September 4, 2026, Anthropic shared the first complete computer-checked proof of Fermat's Last Theorem. Claude wrote 13 million lines of Lean over 11 days, proving 30,300 theorems (29,500 used in the final proof), and Lean checked it using only its three standard axioms.

How did Claude prove Fermat's Last Theorem in Lean?

A team of Claude agents worked through Prove2Me, a DAG-based collaborative formalization platform, consuming about 6 billion output tokens from an internal research model comparable to Claude Fable 5.1. The proof follows the Darmon-Diamond-Taylor simplification of Wiles's proof, with human input limited to occasional high-level instructions.

What does the Fermat's Last Theorem proof mean for AI and mathematics?

It demonstrates that large-scale autoformalization is now feasible, which reduces the burden of refereeing new mathematical work and makes LLM-generated proofs machine-checkable. Kevin Buzzard said this is a big step toward automatic formalization of the modern mathematical literature, and it lands one day after OpenAI's PrimeGaps186 Lean artifact, making formal math a frontier-lab battleground.

Fermat's Last Theorem: Claude's 13M-Line Lean Proof

Yesterday OpenAI took a conditional swing at prime gaps in Lean. Today Anthropic finished something bigger: the first complete computer-checked proof of Fermat's Last Theorem. Claude did it largely autonomously in 11 days — 13 million lines of Lean, 30,300 theorems proved along the way, 29,500 in the final artifact. Kevin Buzzard reviewed it. The repo shipped this morning and cleared 370 points on HN within hours.

What shipped

anthropics/fermats-last-theorem formalizes a simplified version of Wiles's proof via the Darmon–Diamond–Taylor route. The headline numbers: 13M lines (5x the size of Mathlib itself), ~6 billion output tokens from an internal research model "roughly comparable to Claude Fable 5.1," and a comparator confirming the proven statement matches Mathlib's own statement of FLT. Only Lean's three standard axioms, nothing else.

The engineering detail worth stealing: the first agent runs failed — they lost track of project state and stopped collaborating, and their failed attempts still make up ~7% of the final non-boilerplate lines. The win came from Prove2Me, Tianyi Peng's open platform that keeps a DAG of theorem statements so agents can pick what to prove next without memory drift. The human blueprint for this project was an 86-page document expected to take years. Claude's answer: 11 days.

Why it matters

Look at the last 48 hours: OpenAI's PrimeGaps186 = new math, conditional on unformalized axioms. Anthropic's FLT = old math, verified end-to-end. Two labs, two Lean artifacts, two different bets on where formal verification pays. The first argues machines can discover; the second argues machines can check — and checking is now cheap enough that the entire 358-year-old corpus is in scope.

Buzzard's line is the one to clip: if FLT autoformalizes now, automatic formalization of the modern mathematical literature is a step away. That kills the referee bottleneck — and gives every LLM-generated proof a tripwire. Expect theorem-proving suites to become a standard model benchmark by next quarter.

Verdict

Formal math just became the frontier-lab battleground. This isn't a curiosity — it's the first artifact that makes AI-produced mathematics cheaper to trust than human-produced mathematics.

What shipped

Why it matters

Verdict

Related Reading