DEV Community

Cover image for Lean 4 proof of Fermat's Last Theorem: how Claude did it in 11 days
Nikoloz Turazashvili (@axrisi)
Nikoloz Turazashvili (@axrisi) Subscriber

Posted on

Lean 4 proof of Fermat's Last Theorem: how Claude did it in 11 days

#ai #claude #programming #news

On September 4, 2026, Anthropic published a complete Lean 4 proof of Fermat's Last Theorem: 13 million lines, written largely by Claude agents in 11 days, and checked by a machine rather than by referees. The mathematician who has led the human effort to do the same thing since 2024 confirmed that it checks out, and then wrote that it tells us "essentially nothing" about mathematics. Both are true, and the gap between them is the interesting part for anyone who writes software that has to be correct.

TL;DR

  • Anthropic says dozens of Claude agents produced 13 million lines of Lean, 29,500 intermediate theorems and about 6 billion output tokens. That is over five times the size of Mathlib, Lean's whole mathematics library.
  • The build fails unless the proof depends on exactly Lean's three standard axioms: no sorry, no native_decide.
  • A from-scratch build took 5 h 32 min on 96 jobs and peaked at 153 GB of RAM. The theorem names are machine-generated: the repo says it is "written to be checked rather than read".
  • Kevin Buzzard, who had a £1 million, five-year grant for the same goal, verified it and called it mathematically empty but a real step for autoformalization. A commenter's list-price estimate for the tokens: about $300,000.
  • The same day, world number one Shin Jin-seo beat KataGo 2–1 at Go with a two-stone handicap.

What is Fermat's Last Theorem?

The statement fits on one line: no positive integers a, b and c satisfy aⁿ + bⁿ = cⁿ for any integer n greater than 2. Pierre de Fermat wrote it in a book margin around 1637 and claimed a proof the margin was too small to hold. A 1908 prize of 100,000 gold marks attracted 621 incorrect proofs in its first year.

Andrew Wiles announced a proof in June 1993. A gap was found, he fixed it with Richard Taylor, and the result was published in May 1995: 129 pages that, in Anthropic's words, took "months of painstaking work to verify". Nobody seriously doubted it after that. The doubt was never whether the theorem is true. It was whether any single human could check every step.

What does it mean to formalize a proof in Lean 4?

Lean is a proof assistant: a programming language whose type checker also checks mathematics. You write the theorem as a type, write the proof as a program, and the Lean kernel refuses to compile anything with a gap. Formalizing means rewriting a human proof at that level of detail, down to every lemma a textbook would call obvious.

This is the statement Anthropic's repo proves, from its FinalCheck.lean:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem
Enter fullscreen mode Exit fullscreen mode

The second half matters most. #print axioms lists everything the proof ultimately assumes, and #guard_msgs makes the build fail if that list differs from the expected one. propext, Classical.choice and Quot.sound are Lean's standard axioms. sorry is Lean's placeholder for "trust me", and native_decide hands a computation to compiled code outside the kernel. Neither appears, so the checker's answer is not "probably" but "yes, given these three axioms and this statement".

Kevin Buzzard at Imperial College London has led a human project to formalize the theorem since 2024 (GitHub). Its blueprint, the plan alone, runs to 86 pages, and the work "was expected to take years".

How Claude proved Fermat's Last Theorem in Lean

Anthropic's research post describes "dozens of Claude agents" running in a Claude Code multi-agent harness on Prove2Me, a platform from Tianyi Peng of Columbia. Prove2Me keeps a directed acyclic graph of theorem statements, with Fermat's Last Theorem at the root and the lemmas it depends on below, so each agent knows what is still open and what to prove next. The model was "a general-purpose internal research model roughly comparable to Claude Fable 5.1".

The graph exists because the first attempts failed. Early agents "lost track of the project's state and stopped collaborating". Those runs still contributed about 7 % of the non-boilerplate lines. Human input was limited to "occasional high-level instructions" from Peng, such as "Jacobian as a scheme sounds high priority". The proof follows the 1995 Darmon–Diamond–Taylor exposition of Wiles and Taylor–Wiles.

After 11 days, at 02:00:57 UTC on August 18, "The FLT root reads PROVED". Anthropic announced it on September 4.

Lean's own account: 13 million lines of Lean, 29,500 intermediate theorems,

How do you check a 13-million-line proof?

You don't read it; you rebuild it. The repository README gives the numbers:

Check Result
Lean version, modules 4.33.1, 60,475 modules
From-scratch lake build 5 h 32 min at 96 jobs, peak 153 GB RAM
comparator replay 14 h 46 min, peak 230 GB RAM
nanoda, an independent kernel in Rust "Checked 1,052,234 declarations with no errors"
Axioms exactly propext, Classical.choice, Quot.sound

The independent kernel is the part to notice. If Lean's own kernel had a bug, a second implementation written separately would be unlikely to share it. The trust you need shrinks to three things: the statement on the first line of the code block above, the three axioms, and two small kernels.

What you give up is readability. The README says the names are machine-generated and the code is "written to be checked rather than read". It is a "Research artifact. Not maintained and not accepting contributions."

Kevin Buzzard: "essentially nothing", and why he's excited anyway

Buzzard's post is titled "FLT: Anthropic has beaten me to it". Anthropic lent him a machine with 500 GB of RAM. He compiled "over 13.4 million lines", which took "nearly 20 times as long to compile as Lean's mathematics library (on a machine with 96 cores!)", ran comparator, and reported: "it checks out".

Then: "Note that mathematically this work of anthropic tells us essentially nothing". He was "99.9% sure" the theorem was fine and number theorists were "100% sure"; the formalization "just faithfully follows the early literature on the proof and adds nothing." Anthropic's post says proof assistants demonstrate a proof's "correctness beyond a doubt". For this theorem there was little doubt to remove.

What it does show is how far autoformalization has come, and that is the part he is excited about. It also completes the last of Freek Wiedijk's 100 formalization challenges, a list about 20 years old.

On money he wrote: "I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…" Anthropic gave tokens, not dollars. In the comments David Jao estimated 6 billion output tokens at API prices at about $300,000, and HN user sebzim4500 reached the same figure at $50 per million output tokens. That excludes training the model.

My favourite detail: the email telling him arrived while he was at the Green Man festival in Wales with poor 4G, from "someone I'd never heard of", and he "wrote them off as a crank".

What formal verification means for developers

This was mathematics, but the pattern is familiar from software.

  • The statement is the spec, and it is the only part you must read. Thirteen million lines are trusted because a short theorem and three axioms are. In code, the equivalent is a small, reviewed specification with a machine checking the implementation against it.
  • Machine-written, machine-checked works when the checker is strict. The agents could write unreadable code because Lean rejects anything with a gap. Without a checker of that quality, the same volume of generated code is a liability.
  • Coordination was the hard problem. The agents failed until they had a shared graph of what was proved and what was open. If you run multi-agent coding, the task graph is the product.

Shin Jin-seo beats KataGo: humans went one for two

On the same front page (HN), a human won one back. Shin Jin-seo, 26, a 9-dan and the world's top-rated Go player, beat KataGo, the strongest open-source Go engine, two games to one in Seoul in July, taking black plus two stones (KED Global). Two stones is roughly the historic gap between a top professional and a new one.

He lost game one badly, won game two by 4.5 points, and won the decider by 11.5 points in 221 moves, holding a 99 % win probability from mid-game after "a measured attack on move 80". The prize was 250 million won, about $170,000, plus a Genesis G90. His explanation: "rather than trying to imitate AI, it is far more important to build the board according to my own style."

Also in this episode: Chrome 152, Mullvad DNS, React Compiler in Vite, IBM Bob

Chrome 152 (release notes) shipped 12 security fixes. CVE-2026-85046, a type confusion in V8, earned its reporter $1,000, and "Google is aware that an exploit for CVE-2026-85046 exists in the wild." Update, and note that Shin's prize was 170 times the bounty.

Mullvad is shutting down its public encrypted DNS on November 2 and sponsoring Quad9 instead. If you hard-coded its DoH servers, change them before then.

The Rust React Compiler is native in Vite. @vitejs/plugin-react 6.1.0 takes { compiler: true } to use oxc's compiler. On a 1,036-file codebase the compile step went from 14.3 s to 0.81 s, and the full build from 22.1 s to 9.3 s (write-up).

IBM Bob (bob.ibm.com) greets you with "Hi, I'm Bob!", runs subagents, targets Java and mainframe modernization, and ships an analytics product called Bobalytics.

Verdict: SHIP IT

I stamped it SHIP IT. The kernel says yes, an independent kernel says yes, and Buzzard says yes. The mathematics did not change. The way we check mathematics did: a proof nobody will ever read can now be trusted further than one a few experts read, as long as the statement and the axioms are right.

FAQ

Did AI prove Fermat's Last Theorem?
No new proof. Claude formalized Wiles and Taylor's existing proof in Lean 4, so a machine could check every step.

How long is the Lean proof of Fermat's Last Theorem?
About 13 million lines of Lean with 29,500 intermediate theorems, over five times the size of Mathlib.

Can I check the proof myself?
The repo is public. The README reports a 5.5-hour build on 96 jobs with 153 GB of RAM peak, so you need a large machine.

Sources

This article expands on an episode of **The Daily Diff, a five-minute daily video on what shipped and what broke in tech.
Watch the episode · Subscribe on YouTube · the written diff lands in your inbox every morning at thedailydiff.dev.

Top comments (0)