Claude proved Fermat's Last Theorem in 11 days: and a computer checked every step
Anthropic's multi-agent Claude system produced a machine-verified formal proof of Fermat's Last Theorem in 11 days, writing 13 million lines of Lean 4 code.
Fermat’s Last Theorem is arguably the most famous unsolved problem in mathematical history. Pierre de Fermat scribbled a conjecture in a margin around 1637, and it took until 1995 for Andrew Wiles to produce a 129-page proof that finally settled it. Getting that proof checked by a computer, line by line, was expected to take a team of mathematicians several more years.
A multi-agent Claude system did it in 11 days.
Anthropic published the result on 4 September 2026, releasing the complete Lean 4 proof on GitHub under the Apache-2.0 licence. The proof has been verified by Lean’s own kernel, confirmed by an independent second checker called nanoda, and reviewed by Kevin Buzzard of Imperial College London, one of the world’s leading experts in formal mathematics.
What does “formalising a proof” actually mean?
A mathematical proof written on paper is convincing to other mathematicians, but it still relies on human judgement. Formalisation converts that reasoning into a form a computer can check mechanically, with no room for hand-waving. The tool used here is Lean 4, a proof assistant that accepts only logically airtight steps.
The challenge with Wiles’s proof is its sheer scope. It draws on elliptic curves, modular forms, Galois representations, and a chain of deep results spanning decades of number theory. Encoding all of that had been a multi-year community project, led by Buzzard’s team at Imperial College London. The expectation was that finishing the job would take years more.
How the system worked
The project was initiated by Tianyi Peng, an Anthropic researcher who also runs a group at Columbia University building tools for AI formalisation. He paired a Claude Code-based multi-agent workflow with Prove2Me, an open platform he developed for coordinating AI agents on large proof tasks.
Prove2Me tracks how different parts of a proof depend on one another, maintains natural-language descriptions of each theorem so agents can search and reuse existing results, and speeds up Lean compilation by separating theorem statements from their proofs. Without it, an earlier attempt by the team had failed.
Dozens of agents ran in parallel across the 11 days, each working on different sub-problems. The wall-clock time was short, but the compute was substantial: roughly six billion output tokens from an internal research model broadly comparable to Claude Sonnet-class capability.
The numbers are striking. The system wrote 13 million lines of Lean 4 code, proved 30,300 theorems (29,500 of which appear in the final proof), and produced what Anthropic describes as the largest single file of Lean code ever written. For comparison, all of Mathlib, the community library of formalised mathematics that has been built up over years, is about one-sixth the size.
Human input was deliberately minimal. Tianyi provided occasional high-level direction, such as “Jacobian as a scheme sounds high priority” and “push the Mazur theorem to be done soon.” Everything else was handled by the agents.
The verification chain
One reasonable question is: how confident can we be the proof is actually correct?
The answer is unusually thorough. Lean’s kernel accepted every declaration. An independent second checker, nanoda, did the same. A separate comparator confirmed that the theorem statement proved matches the standard statement of Fermat’s Last Theorem already in Mathlib’s library. The root theorem reads “Proved” on Prove2Me, meaning every node in its dependency tree, covering results including the Mazur theorem, Ribet’s level-lowering theorem, and Langlands-Tunnell, has a machine-checked proof. The entire edifice rests on Lean’s three standard axioms and nothing else.
Buzzard put it plainly: “This extraordinary autoformalization achievement proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics.”
This also closes a 20-year benchmark. Fermat’s Last Theorem was the final entry on Freek Wiedijk’s list of 100 theorems that computer scientists had proposed as formalisation targets. Every theorem on the list now has a machine-checked proof.
What this means for you
The immediate beneficiary is the mathematical community, but the implications reach further.
For mathematicians, the significance is that a process expected to take years of careful human work was completed in under a fortnight. Buzzard noted that autoformalization techniques “will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees.” Mathematical peer review is slow and error-prone precisely because human referees cannot check every detail of a complex proof. Machine verification removes that bottleneck.
For anyone following AI development, the more interesting signal is about what multi-agent systems can now do on long-horizon technical tasks. This was not a benchmark prompt answered in seconds. It was 11 days of largely autonomous work, coordinating dozens of agents, managing dependencies across tens of thousands of sub-problems, and producing output at a scale no human team would attempt. The agents had to decide what to work on, search for reusable results, handle dead ends, and keep the overall structure coherent.
For software and research teams more broadly, Prove2Me’s approach to coordination, tracking dependencies, maintaining searchable descriptions of intermediate results, and separating concerns to allow parallel work, is the kind of scaffolding that makes large autonomous tasks tractable. That pattern is likely to appear in other domains.
One thing worth being clear about: Claude did not discover Fermat’s Last Theorem. Andrew Wiles did that in 1995. What this system did was take an existing, accepted proof and encode it in a form a computer can verify without any human trust. That is a different achievement, and in many ways a more practically useful one, because verification is the bottleneck that matters for building reliable knowledge at scale.
The complete proof, a walkthrough in PROOF-PATH.md, and an offline HTML browser covering every theorem and its dependency graph are all available at github.com/anthropics/fermats-last-theorem.