Claude Formalized Fermat’s Last Theorem. It Did Not Discover a New Proof.

Anthropic says Claude has produced the first complete, computer-checked formalization of Fermat’s Last Theorem.

The scale is difficult to ignore: 11 days, roughly six billion output tokens, 13 million lines of Lean, and 29,500 intermediate theorems used in the final proof. Dozens of agents worked in parallel. A Lean kernel accepted the result.

But the cleanest interpretation is not “AI solved Fermat’s Last Theorem.” The theorem was solved by Andrew Wiles and Richard Taylor three decades ago, building on generations of mathematics. Claude followed an existing proof route and translated it into a form a proof assistant could check.

That is still a major result. It is simply a different result.

What Anthropic actually released

On September 4, Anthropic announced what it describes as the first end-to-end, computer-checked proof of Fermat’s Last Theorem.

The public Lean repository contains the theorem statement, definitions, intermediate theorems, proof files, a proof-path guide, and verification tooling. According to the repository:

• the default build checks 60,475 modules;
• the final artifact contains 29,511 theorem pages;
• the proof uses Lean’s three standard axioms: propositional extensionality, classical choice, and quotient soundness;
• the build rejects placeholders such as sorry and added axioms;
• Lean’s kernel checked every declaration;
• a comparator matched the proved statement to Mathlib’s statement of Fermat’s Last Theorem; and
• a second kernel, nanoda, accepted an export containing more than one million declarations.

Anthropic reports that mathematician Kevin Buzzard reviewed the artifact and called it a significant autoformalization achievement. The code is public, which makes the core claim unusually inspectable for an AI research announcement.

It is not yet the same thing as broad independent replication. The repository was published by the team making the claim, and rebuilding the full verification stack requires substantial hardware. But it gives outside researchers far more to examine than a benchmark chart or a demonstration video.

The three layers people keep collapsing

To understand the result, separate three different activities.

1. Discovering a theorem

This means identifying a new mathematical statement that appears to be true. Fermat’s Last Theorem was already known as a statement for centuries.

2. Finding a proof

This means constructing the mathematical argument that establishes the statement. Wiles’s proof, completed with Taylor, did this using modern number theory. Anthropic says Claude followed a simplified exposition of that established route by Darmon, Diamond, and Taylor.

3. Formalizing and checking the proof

This means expressing the definitions and logical steps in a formal language precise enough for a small verification kernel to check mechanically.

Claude’s contribution is primarily in the third layer.

That layer is not clerical transcription. Human mathematical writing leaves many steps implicit, relies on shared conventions, and builds on results scattered across a large literature. A proof assistant requires definitions, types, dependencies, and logical transitions to be explicit. Filling that gap at this scale is genuine technical work.

But formalization and discovery answer different questions.

A new proof asks: Can we find a valid path to the theorem?

A formal proof asks: Can every step in this specified path be reduced to rules the kernel accepts?

What the kernel checked—and what it did not

A proof assistant changes the trust model.

Instead of asking readers to inspect 13 million lines manually, the system asks them to trust a much smaller core: the theorem statement, the formal definitions it refers to, the axioms permitted, and the correctness of the verification kernel.

The repository’s final check is designed to show that the theorem depends only on Lean’s standard axioms and that no prohibited escape hatch was used. Comparator checks that the submitted theorem is the same challenge statement expressed through trusted Mathlib definitions. Nanoda supplies a second implementation of a Lean kernel.

This is strong engineering around a familiar failure mode: proving the wrong statement correctly.

Still, a kernel does not understand mathematical intention. It verifies syntax, types, and logical derivations. It cannot tell whether an intermediate theorem’s English label accurately describes its formal content. The repository says this directly: where a generated name and its statement disagree, the formal statement is authoritative.

This distinction should feel familiar to data practitioners. A query can execute perfectly against the wrong table. A model can optimize the wrong label. A test suite can pass while encoding the wrong business rule.

Formal verification makes execution errors much harder. It does not eliminate specification errors.

Thirteen million lines is not the quality metric

The largest number in the announcement may also be the least useful one.

Anthropic says the artifact is more than five times the size of Mathlib, the main community library on which it builds. That sounds like a measure of intellectual scale. It is partly a measure of machine-generated redundancy.

The repository describes the Lean sources as written to be checked rather than read. Anthropic notes that the proof is probably much longer than necessary. About seven percent of the non-boilerplate lines in the final artifact came from failed early attempts.

For human software, 13 million lines would usually increase concern. More code means more surface area to review and maintain. Formal proof changes the economics because the kernel, not a person, checks the logical object.

That creates a new optimization problem. If generation becomes cheap and verification remains reliable, systems may produce vast artifacts that are correct but difficult to understand, compress, reuse, or maintain.

The next metric should not be lines generated. It should be how much trusted, reusable mathematical structure survives after compression and expert review.

The scaffold mattered as much as the model

Anthropic reports that early agent attempts lost track of state and stopped collaborating effectively. The project succeeded after the team moved to Prove2Me, an open platform for collaborative formalization.

Prove2Me maintained a directed acyclic graph of theorem statements. That graph gave agents a shared map of what was proved, what remained open, and which dependencies were blocking progress. The platform also separated statements from proofs, accelerated compilation, and attached natural-language descriptions that improved search and reuse.

This is the same pattern that appears across serious agent systems:

Failure	Scaffold response
agents forget project state	externalize state in a shared graph
workers duplicate effort	assign tasks against explicit dependencies
context becomes too large	separate statements, proofs, and summaries
errors propagate silently	require machine-checkable completion criteria
parallel work becomes chaotic	coordinate through a common artifact store

The model generated the proof. The scaffold made the work legible and composable.

That matters beyond mathematics. When a long-running agent project succeeds, the causal unit is rarely “the model” alone. It is the model, state representation, task decomposition, toolchain, verifier, and human steering.

Why this matters outside pure mathematics

Formal mathematics offers an unusually favorable environment for AI-generated work because correctness can be checked by a deterministic kernel.

Most knowledge work has no equivalent.

A generated market analysis cannot be reduced to a type check. A policy recommendation has contested objectives. A medical conclusion depends on measurement quality, population assumptions, and consequences that a compiler cannot see.

The Fermat project therefore teaches two lessons at once.

First, AI can generate far more complex verified artifacts when the domain has a precise language and a strong validator.

Second, the validator is doing a large share of the safety work.

For data and ML teams, the practical question is: What is your kernel?

It might be:

• a schema and data-contract test suite;
• a holdout dataset that was never used for tuning;
• a simulator with known invariants;
• a compiler and static type checker;
• a reproducible build;
• a policy engine with explicit constraints; or
• a human approval boundary for claims that cannot be mechanically verified.

The replication cost is part of the story

The repository is public, but verification is not lightweight.

Its instructions say a full build used 96 parallel jobs, peaked at 153 GB of memory, and temporarily produced roughly 220 GB of C files. The comparator run took nearly 15 hours on one core and peaked at 230 GB of memory. The maintainers recommend allowing 300 GB.

That does not invalidate the result. It narrows who can independently reproduce the exact verification today.

Public code is necessary for scrutiny, but practical reproducibility also depends on compute, storage, pinned dependencies, documentation, and accessible verification paths. A result that only a few institutions can rebuild remains more inspectable than a closed demo, but less broadly reproducible than a small artifact.

A useful next step would be third-party rebuilds, reduced proofs, and independently maintained verification recipes.

What would make me wrong

My cautious interpretation would be too narrow if the artifact contains substantial novel mathematical ideas rather than primarily a formalization of the established route.

I would update if expert reviewers identify new lemmas, abstractions, or proof strategies that materially improve human understanding of Fermat’s Last Theorem or related mathematics.

I would also become more confident in the broader significance if:

• independent teams reproduce the full build and comparator checks;
• the formalization is accepted and maintained by the relevant Lean and Mathlib communities;
• large parts of the artifact are compressed into reusable libraries;
• the same workflow formalizes other major results at lower cost; and
• researchers demonstrate that formalization catches consequential errors in published mathematics.

Conversely, the result would look weaker if independent auditors find a mismatch between the intended theorem and the checked statement, an unsound dependency, or verification behavior that relies on a bug in the toolchain.

The right headline

Claude did not solve Fermat’s Last Theorem in 11 days. It did not replace Wiles’s mathematical discovery.

It produced a public, machine-checked formal artifact of an existing proof path at a scale and speed that would recently have sounded implausible.

That is a narrower claim than the viral version. It may also be the more important one.

As AI systems generate more mathematics, code, analyses, and scientific hypotheses, producing candidate work will become cheaper. The scarce resource will be trustworthy evaluation.

The Fermat result is not just a story about what an AI generated. It is a story about what a verifier made safe to believe.

Sources

• Anthropic — Formalizing Fermat’s Last Theorem
• Anthropic — Fermat’s Last Theorem in Lean 4 repository
• Lean Prover — Comparator
• Chen et al. — Prove2Me: An Open Collaborative Platform for Scaling Math Formalization