Fermat’s Last Theorem was solved decades ago. What changed in 2026 is that the proof can now be checked end to end by a computer.
Anthropic says Claude worked largely autonomously for 11 days to produce the first complete machine-checked Fermat’s Last Theorem proof in Lean. The project generated about 13 million lines of Lean, proved roughly 30,300 intermediate theorem statements, and used about 29,500 in the final proof. The key point is easy to lose: Claude did not discover a new solution. Andrew Wiles, with Richard Taylor, settled the theorem in the 1990s.
Claude instead translated a huge body of modern reasoning into a formal object that Lean’s kernel could check line by line. The achievement is not “AI finally solved Fermat.” It is autoformalization at a scale that recently looked like a multi-year human project.
Table of Contents
1. Fermat’s Last Theorem Proof: What Changed in 2026?
Fermat’s Last Theorem says there are no positive integers a, b, and cthat satisfy a^n+b^n=c^nfor any integer exponent n>2.
The statement dates to Pierre de Fermat’s famous 17th-century margin note in Arithmetica. Its simplicity is part of the legend. The claim is easy to understand, but proving it required centuries of mathematics.
The key distinction is solving the theorem versus formalizing its proof.
Fermat’s Last Theorem Proof: Wiles vs Claude at a Glance
| Question | Wiles/Taylor | Claude/Anthropic |
|---|---|---|
| Did it solve Fermat’s Last Theorem? | Yes | No new solution was needed |
| Was the core mathematics new? | Yes | Primarily no |
| Main output | Human mathematical proof | Machine-checkable Lean proof |
| End-to-end computer checked? | Not in the original publication | Yes |
| Main significance | Solving a centuries-old problem | Large-scale autoformalization |
| Date | Corrected proof published in 1995 | Formalization announced in 2026 |
Wiles announced a proof in 1993, but reviewers found a serious gap. He and Taylor repaired the argument, and the corrected work was published in 1995. That is the Andrew Wiles Fermat’s Last Theorem proof that ended the mathematical problem.
Claude’s contribution came later in the verification layer. It turned an existing modern proof route into formal Lean code that a small trusted kernel could check.
So the 2026 Fermat’s Last Theorem proof is not a replacement for Wiles. It is a machine-verifiable reconstruction of the mathematics that ultimately established the theorem.
That distinction matters because “Claude proved Fermat’s Last Theorem” is technically true in the formal-proof sense, but badly misleading if it implies Claude independently discovered the mathematics.
2. What Anthropic and Claude Actually Formalized
The Claude Fermat’s Last Theorem project follows the modern chain of ideas associated with Frey, Serre, Ribet, Wiles, and Taylor-Wiles, using an exposition by Henri Darmon, Fred Diamond, and Richard Taylor as a guide.
At a high level, the path runs through elliptic curves and modular forms. A hypothetical solution to Fermat’s equation produces a special elliptic curve. Ideas from Gerhard Frey and Jean-Pierre Serre, followed by Ken Ribet’s level-lowering result, connect that curve to the modularity results established through Wiles’s program.
The logic is a contradiction: if a counterexample to Fermat existed, it would imply an elliptic curve that modern modularity theory rules out.
Fermat’s Last Theorem Proof: How the Formalization Works
| Layer | What It Contributes | Why It Matters to the Formalization |
|---|---|---|
| Fermat Equation | Defines the target theorem | The final Lean statement must match it exactly |
| Frey Curve | Turns a hypothetical FLT solution into an elliptic curve | Connects the elementary-looking equation to modern number theory |
| Serre/Ribet Ideas | Restrict the properties such a curve could have | Creates the contradiction route |
| Modularity Results | Show the relevant elliptic curves must be modular | Supplies the deep theorem that closes the argument |
| Lean/Mathlib | Provides formal definitions and checked dependencies | Converts the reasoning into kernel-verifiable proof terms |
| Prove2Me | Organizes theorem dependencies for many agents | Makes large-scale parallel formalization manageable |
Anthropic also did not simply “finish Kevin Buzzard’s project.” Buzzard’s Imperial College effort follows a different modern route and aims to build reusable, carefully structured mathematics for long-term use in Mathlib. Anthropic’s goal was an end-to-end certificate. The projects are related, not interchangeable.
3. How Claude Formalized Fermat’s Last Theorem in 11 Days
The surprising part of the story is not that a language model can write Lean. Models have been doing theorem-proving work for years. The surprising part is coordination.
Early attempts stalled because agents lost track of project state. A proof this large is a dependency graph with thousands of definitions, lemmas, imported results, and subgoals. Duplicate work or incompatible intermediate results can quickly stall progress.
The successful run used Prove2Me, a collaborative formalization platform developed by Tianyi Peng and collaborators at Columbia University, together with a Claude Code-based multi-agent harness.
Prove2Me maintained a directed acyclic graph of theorem statements, giving agents a shared map of dependencies and useful next targets. It also separated statements from proofs, sped compilation, and supported search and reuse.
In practice, the workflow looked less like one genius model writing a 13-million-line file and more like a software build system staffed by dozens of mathematical agents.
Claude agents could:
- define missing mathematical objects,
- select reachable subgoals,
- search for reusable lemmas,
- prove intermediate theorems in parallel,
- feed completed results into harder downstream statements,
- and keep working until the root theorem closed.
Anthropic says the run consumed about six billion output tokens from an internal research model roughly comparable to Claude Fable 5.1. Human mathematical direction was limited and high level. The source describes the successful campaign as dozens of agents using Prove2Me and a Claude Code-based harness.
Anthropic has not disclosed the actual dollar cost. Public API-price calculations can produce eye-catching estimates, but those estimates are not Anthropic’s internal cost and should not be presented as such.
4. Why Did the Fermat’s Last Theorem Proof Need 13 Million Lines of Lean?
The 13-million-line number sounds absurd until you remember how human mathematics is written.
A paper can say “clearly” or “it follows from the previous lemma” because readers reconstruct omitted steps. Authors also rely on a huge shared background without restating it.
Lean does not grade on vibes.
A proof assistant needs the objects, types, dependencies, and logical transformations to be explicit enough for the kernel to verify. If a result depends on a fact that has never been formalized, someone has to formalize that fact too. If a definition differs slightly from the version used elsewhere, the bridge between them may itself need proof.
So 13 million lines does not mean the Fermat’s Last Theorem proof suddenly contains 13 million lines of new mathematical insight. Much of the size comes from making implicit structure explicit, constructing missing infrastructure, and generating code that prioritizes checkability over elegance.
Anthropic also acknowledges that the artifact is likely far more verbose than mature Mathlib code. Mathlib is reviewed, refactored, generalized, and compressed over time. An autonomous campaign trying to close a proof graph in 11 days optimizes for a different target: make the theorem check.
5. Did Claude Really Prove 29,500 New Theorems?
This is another place where a technically correct number can become a bad headline.
Anthropic says Claude produced computer-verifiable proofs for about 30,300 intermediate theorem statements and used roughly 29,500 in the final proof. The repository itself contains 29,511 theorem modules in the import closure of the final check.
That does not mean Claude discovered 29,500 new mathematical truths unknown to mathematicians.
Three ideas need to stay separate:
- a theorem that is newly formalized in Lean,
- a newly generated Lean proof of an existing result,
- a genuinely novel mathematical theorem.
The Claude Fermat’s Last Theorem proof contains enormous amounts of the first two. Anthropic explicitly contrasts this work with research where Claude produced novel mathematics. Here, the novelty is mainly in verification, automation, scale, and speed.
That is still a major result. Formalizing a classical theorem can be hard precisely because the informal literature assumes so much background. But “29,500 new theorems discovered by AI” would overstate what happened.
6. How Do We Know the Fermat’s Last Theorem Lean Proof Is Correct?
This is where the Anthropic Fermat’s Last Theorem claim becomes more interesting than a normal model demo. The result was not accepted because Claude said it was done.
The public repository describes several verification layers.
First, Lean 4’s kernel checks every proof term during a from-scratch build. The final target also checks that the Fermat theorem depends only on Lean’s three standard axioms: propext, Classical.choice, and Quot.sound. The build rejects shortcuts such as sorry or added axioms.
Second, Lean’s comparator checks the theorem against a challenge statement expressed using stock Mathlib. This guards against proving a subtly altered or weaker theorem. The comparator confirmed that the proved statement matches the intended one and replays through Lean’s kernel.
Third, the environment was exported to nanoda, an independent Lean kernel written in Rust. The repository reports more than one million declarations checked without errors.
These layers provide unusually strong evidence that the Fermat’s Last Theorem proof artifact proves the statement it claims to prove under the stated axioms. There is still a software trust base, but this is far stronger than “the code compiled.”
7. Could Claude Have Exploited a Lean Kernel Bug?
The question is reasonable, especially for an artifact this large and machine generated.
Lean has had soundness bugs fixed over its lifetime, and Anthropic’s repository specifically uses Lean 4.33.1, which includes 2026 kernel soundness fixes. So could an AI accidentally or deliberately find a new flaw and use it to prove something false?
In principle, no serious proof assistant should be described as metaphysically bug-free. In practice, there is no evidence that Claude exploited a kernel flaw here.
Confidence comes from a patched Lean version, full proof replay, restricted axioms, statement comparison, and the independent nanoda check.
The “three axioms” language also needs context. Classical.choice, propext, and Quot.sound are standard Lean foundations. The claim means the dependency graph ultimately uses those principles rather than unverified escape hatches.
8. Did Claude Find Fermat’s Lost “Marvelous Proof”?
No.
Claude’s proof uses modern mathematics that Fermat could not have known in 1637. Elliptic curves, modular forms, Galois representations, and the chain of results leading to the Wiles/Taylor-Wiles argument came centuries later.
There is still no known elementary proof based only on mathematics Fermat plausibly had access to. The common historical view is that Fermat either had a mistaken argument or a proof for a narrower case and overgeneralized it.
Could Anthropic have asked Claude to search for a dramatically simpler proof instead? Of course, but that would be a different research task.
Formalizing Fermat’s Last Theorem asks, “Can the machine encode and verify a known route?”
Finding a radically simpler proof asks, “Can the machine discover new mathematics?”
The first task now has a striking answer. The second remains open.
9. Did Claude Make Kevin Buzzard’s Fermat Project Obsolete?
No, and treating the two efforts as a race misses what formal mathematics is for.
Buzzard’s Imperial College project aims to build clean, reusable mathematical infrastructure that strengthens the broader Lean ecosystem. Maintainability, abstraction, reuse, and human comprehension matter.
Anthropic’s artifact was built to reach an end-to-end checked result quickly. Its own repository says the Lean sources are written to be checked rather than read, with machine-generated names and pipeline labels. The project is published as a research artifact and is not maintained.
That difference is important.
A 13-million-line certificate can establish that a theorem follows from its dependencies. A carefully engineered library can become infrastructure for the next hundred theorems. Claude shows how quickly AI can fill a proof graph. Buzzard’s project helps show what durable formal mathematics should look like afterward.
10. Why Claude’s Fermat’s Last Theorem Proof Matters
For Fermat’s Last Theorem itself, the impact is modest. Mathematicians were not waiting to learn whether Wiles was right.
For formal mathematics, AI research, and the future of scientific verification, the impact could be much larger.
The clearest signal is scale. A formalization expected to demand years of specialist work was completed largely autonomously in days. The artifact is huge and expensive in tokens, but it crossed the finish line.
AI systems may now be able to formalize large parts of the mathematical literature when humans provide the right scaffolding. Formal proofs could expose hidden gaps, reduce referee workload, and make future AI-generated mathematics easier to audit.
So, can AI prove Fermat’s Last Theorem? In the formal sense demonstrated here, yes. An AI system can construct an end-to-end proof object that a proof assistant verifies. What it did not do was independently discover the mathematical breakthrough behind the theorem.
That distinction will become more important as AI-generated research scales.
If models become capable of producing more mathematical arguments than humans can realistically review, human-readable prose alone will not scale as a trust mechanism. A plausible future workflow is dual output: an explanation for people and a formal certificate for machines.
That does not make mathematicians obsolete. Formalization can verify that a chain of logic is valid. It cannot decide whether a theorem is interesting, whether the definitions capture the right concept, whether a proof teaches us something, or which research direction deserves attention.
The most useful interpretation of Claude’s Fermat’s Last Theorem proof is therefore not “AI beat Wiles.” It is that AI may have crossed a threshold in turning human mathematics into machine-checkable mathematics.
11. The Real Takeaway
The Fermat’s Last Theorem proof was the benchmark, not the discovery.
Wiles and Taylor supplied the mathematical breakthrough. Claude supplied something different: a demonstration that a multi-agent AI system, given formal tools, a theorem dependency graph, and existing mathematical infrastructure, can convert an enormous modern proof into a complete machine-checkable artifact at surprising speed.
That is a less sensational claim than “AI solved Fermat’s Last Theorem,” but it is more consequential.
If this approach generalizes, the next big change in mathematics may not be an AI suddenly producing a mysterious one-page proof of a famous problem. It may be thousands of ordinary and extraordinary results becoming formally checkable by default.
For developers, researchers, and AI builders, that is the part to watch. The frontier is moving from models that can talk about proofs to systems that can organize, generate, and independently verify proof structures at industrial scale.
Binary Verse AI will keep tracking that shift, including what it means for Lean, AI agents, automated research, and the reliability of machine-generated science. If you want the signal without the hype, follow our latest AI research explainers and technical deep dives.
1. Was Fermat’s Last Theorem ever solved?
Yes. Andrew Wiles announced a proof of Fermat’s Last Theorem in 1993, but a gap was later discovered. Wiles and Richard Taylor repaired the argument, and the corrected proof was published in 1995. Claude’s 2026 achievement did not solve a previously open problem; it produced the first complete machine-checked Lean formalization of an existing proof route.
2. Can AI prove Fermat’s Last Theorem?
Yes, in the sense that AI can now construct a formal proof that a proof assistant can verify step by step. Anthropic’s Claude produced a complete Lean proof of Fermat’s Last Theorem in 2026. However, Claude did not discover the original mathematical solution. The underlying argument comes from work by Andrew Wiles, Richard Taylor, Ken Ribet, Jean-Pierre Serre, Gerhard Frey, and other mathematicians.
3. How long is the proof of Fermat’s Last Theorem?
Wiles’s original published proof spans more than a hundred pages of highly advanced mathematics. Anthropic’s formal version is vastly larger, totaling roughly 13 million lines of Lean code. The difference exists because Lean requires definitions, dependencies, and logical steps that human mathematicians normally leave implicit to be written out explicitly.
4. Did Ramanujan solve Fermat’s Last Theorem?
No. Srinivasa Ramanujan made major contributions to number theory, infinite series, partitions, and modular forms, but he did not prove Fermat’s Last Theorem. The first accepted general proof was produced by Andrew Wiles, with Richard Taylor helping repair a gap in the original argument.
5. What is the hardest theorem in mathematics?
There is no universally accepted “hardest theorem” in mathematics because difficulty can mean different things, such as proof length, conceptual depth, technical complexity, or the amount of prerequisite mathematics required. Fermat’s Last Theorem is one of the most famous difficult problems because its statement is simple, yet proving it required more than three centuries of mathematical development.