Claude formalized Fermat's Last Theorem in Lean in 11 days, according to Anthropic. The achievement is real, but the verb matters: Claude did not discover a new proof of an unsolved problem. It converted a known proof route into a complete machine-checkable artifact. Its importance lies in the system that turned uncertain work by dozens of agents into a result that Lean could check, while leaving human meaning, maintainability, and independent replication as separate questions.
The headline needs the right verb
Fermat's Last Theorem was proved by Andrew Wiles and Richard Taylor in the 1990s. Anthropic's project formalized the Frey, Serre, Ribet, Wiles, and Taylor-Wiles argument, largely following the exposition by Henri Darmon, Fred Diamond, and Richard Taylor.
The run began early on August 7, 2026. The final theorem was marked proved on August 17 at 10:00:57 p.m. Eastern time. Anthropic describes that interval as 11 days of largely autonomous work. Humans supplied the one-line goal and occasional priority guidance. The system also depended on Mathlib and adapted material from the Imperial College London FLT and flt-regular projects.
The scale has several different denominators:
| Metric | Supported claim |
|---|---|
| Output tokens | About 6 billion, reported by Anthropic |
| Lean source | About 13 million lines, including about 10.5 million non-boilerplate lines |
| Theorems proved during the run | About 30,300 |
| Theorems in the final dependency tree | Exactly 29,511 in the released documentation |
| Claude agents | Dozens; Anthropic has not disclosed an exact count |
The model was an internal general-purpose research model that Anthropic says was roughly comparable to Claude Fable 5.1. That wording does not identify it as Fable 5.1. The six-billion figure refers to output tokens, not total tokens or training compute.
What the released theorem says
The public repository declares the elementary statement directly: for every natural number n ≥ 3 and positive natural numbers a, b, and c, aⁿ + bⁿ ≠ cⁿ. FinalCheck.lean then derives Mathlib's own FermatLastTheorem statement from it.
The proof is complete in scope, but famous intermediate results are proved only at the strength this route needs. PROOF-PATH.md specifies the boundary: irreducibility for the relevant Frey curves, particular modularity-lifting and Langlands-Tunnell cases, and level lowering for the Frey representation. It does not claim the most general form of every named theorem.
That distinction is one reason formal verification needs more than a green build. The kernel checks the literal declarations. Human readers still have to verify that names, descriptions, and claimed mathematical scope match those declarations.
Prove2Me turned the proof into a dependency system
Anthropic's first attempts produced local progress but poor global coordination. Agents lost track of project state and stopped reusing one another's results effectively. The successful run used Prove2Me, which separates theorem statements from their proofs and organizes them as a directed acyclic graph.
A proof sketch can close a parent conditionally by importing child statements. Each unresolved child becomes a work item. Immutable statements provide stable targets, natural-language descriptions support search and reuse, and milestones keep parallel workers aligned with a curated route.
This is the central systems result. More agents increased search bandwidth only after the project had a shared state model and a compositional completion rule. Anthropic reports that failed early attempts still contributed about 7% of the final non-boilerplate lines. Failure was useful once its surviving work could enter a stable dependency structure.
This complements our dual-loop protocol for mathematical AI agents. Here the narrower lesson is that a theorem DAG can be a work queue, memory system, reuse index, and executable completion contract.
A root marked proved was still an intermediate state
The most revealing detail appears in Anthropic's run timeline. When the final Prove2Me card switched to proved, the platform had checked each card separately against the statements of its children. That was not yet a single end-to-end Lean build.
The team then fetched and recompiled all 29,511 cards outside the platform, checked the dependency graph, deduplicated the development, and assembled one Lean project. Only after that project built with the expected axiom report did the root become a coherent released artifact.
Local correctness does not establish integration correctness. Every node can appear closed while an export has missing edges, mismatched types, a cycle, or a different top-level statement. Moving from card acceptance to a frozen repository was another verification boundary.
Five checks, five failure surfaces
The released artifact uses several checks that are often compressed into one phrase, computer verified. They provide different guarantees.
| Layer | What it checks | What remains outside it |
|---|---|---|
| DAG closure | Every required leaf is closed and dependencies compose | Whether the statements express the intended mathematics |
| Lean build and axiom print | Proof terms type-check and the final theorem uses only propext, Classical.choice, and Quot.sound |
A bug in the kernel or semantic drift in definitions |
| Mathlib comparator | The top-level statement and referenced constants match a challenge stated using stock Mathlib | Whether every intermediate theorem name describes its literal statement |
| nanoda replay | A separate Rust implementation of a Lean kernel accepts the exported environment | Risks shared by the specification, export path, or checking assumptions |
| Human mathematical review | The formal statements, classical proof route, and advertised scope make mathematical sense | Broad community review and independent full reproduction |
The repository reports a from-scratch build of 60,475 modules on Lean 4.33.1 and Mathlib v4.33.0. It also reports that leanprover/comparator replayed the full environment and confirmed statement identity. nanoda, an independent Lean kernel implementation in Rust, accepted 1,052,234 declarations. Anthropic used four published nanoda patches for progress reporting and performance, and says none changed a typing rule.
Unlike the unit-distance breakthrough, this was not new mathematical discovery followed by expert evaluation. The primary verification object here is an executable proof environment.
Independent verification is not one yes-or-no field
The proof has strong machine-verification evidence. The label independently verified requires more precision.
Lean, comparator, and nanoda are distinct checking paths, and comparator and nanoda were developed outside Anthropic. The published results of running them on this artifact, however, come from the releasing team. Kevin Buzzard provided external expert review and is quoted by Anthropic as confirming that the artifact proves FLT from the standard mathematical axioms. That is meaningful outside scrutiny, but the public record does not show him or another independent team publishing a complete build, comparator, and nanoda rerun.
The repository's own formalization.yaml therefore matters. It marks the review status as self-assessed and lists no reviewers. As of September 5, 2026, there is no public record located in this review of a full independent reproduction or formal peer review.
Reproduction is possible but expensive. Anthropic reports that its build took 5 hours 32 minutes at 96 jobs with 153 GB peak memory. Comparator took about 14 hours 46 minutes and peaked at 230 GB. The nanoda path first writes a 37.8 GB export. Public commands create the possibility of independent verification. A published rerun would supply the next evidence layer.
The distinction resembles the evidence stack in our analysis of Claude's Riemann zeta result: proof generation, statement fidelity, expert review, and external replay are related, but none substitutes for the others.
The public Prove2Me state does not match the release
There is one unresolved discrepancy. On September 5, the public Prove2Me FLT mission still showed the goal as OPEN, with open frontier nodes. The homepage state showed conquered:false, 87 theorems, and two active users. Meanwhile, Anthropic's repository contains a complete 29,511-theorem dependency tree and end-to-end checks.
The public sources do not explain whether the visible mission is an older project, a different instance, or an unsynchronized state. The two active users are not an agent count. This mismatch does not erase the released Lean artifact, but it prevents the public platform page from serving as independent evidence that the run completed.
Thirteen million lines are evidence and maintenance debt
The codebase demonstrates proof production far beyond the scale of manual review. It also exposes the next bottleneck.
The README calls the repository an unmaintained research artifact. Names are machine-generated, and statements are authoritative when names and meanings diverge. The release attributes 106 adapted files to the Imperial FLT and flt-regular projects, on top of Mathlib.
Kernel acceptance establishes formal correctness of the encoded theorem. It does not make 13 million lines concise, reusable, or ready for Mathlib. As proof generation becomes abundant, abstraction, semantic auditing, attribution, and long-term maintenance become scarce. That is the larger shift behind the 11-day headline.
FAQ
Did Claude prove Fermat's Last Theorem?
Claude formalized a complete proof in Lean. Wiles and Taylor proved the theorem in conventional mathematics in the 1990s.
Did Claude discover a new proof?
No. The artifact follows the established Frey, Serre, Ribet, Wiles, and Taylor-Wiles route, largely through the Darmon, Diamond, and Taylor exposition.
How many Claude agents worked on it?
Anthropic says dozens. It has not published an exact count, so a more precise number is unsupported.
What did Lean verify?
Lean checked that the encoded FLT statement follows from the released definitions, dependencies, Mathlib, and three standard axioms, with no proof placeholders in the package.
Has an independent team reproduced the full verification?
No public full rerun was located as of September 5, 2026. The artifact has multiple machine checks and external expert review, while its metadata still says self-assessed.
Why does Prove2Me still show the mission as open?
The public sources do not explain the mismatch. It should be reported as unresolved rather than used to infer that either the public mission or released repository is false.
References
- Anthropic, Formalizing Fermat's Last Theorem
- Anthropic, Run timeline and selected Claude excerpts
- Anthropic, Fermat's Last Theorem in Lean 4 repository
- Anthropic, The route of the proof
- Chen et al., Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
- Prove2Me, Public Fermat's Last Theorem mission