⏱️ Lectura: 10 min
It took Claude eleven days to write what the mathematical community estimated would take years: a complete proof of Fermat’s Last Theorem that a computer can verify step by step, without relying on any human’s word.
📑 En este artículo
Anthropic announced the result on September 4, 2026: Claude agents, working largely autonomously, translated the complete mathematical reasoning into the language of the Lean proof assistant, generating 13 million lines of verified code.
TL;DR
- Claude wrote the first proof of Fermat’s Last Theorem automatically verifiable by a computer.
- The work took 11 days of Claude agents operating largely autonomously.
- The final proof uses 29,500 intermediate theorems out of a total of 30,300 proved in the process.
- The generated Lean code totals 13 million lines, more than 5 times the size of Mathlib.
- The proof follows a simplified version of Wiles’s argument according to Darmon, Diamond, and Taylor.
- Kevin Buzzard, leader of the FLT formalization project in Lean since 2024, validated the result.
- Anthropic published the announcement on September 4, 2026 on its research site.
Introduction
Fermat’s theorem is the claim that Pierre de Fermat scribbled around 1637 in the margin of his copy of Diophantus’s Arithmetica: there are no positive integers a, b, and c that satisfy a^n + b^n = c^n for any n greater than 2. Fermat added a note that became legendary, claiming to have discovered a truly marvelous proof that the margin was too narrow to contain. That line fueled 358 years of attempts, most of them unsuccessful.
What Anthropic announced is not a new mathematical proof. It’s the formalization of an existing proof: converting Andrew Wiles’s reasoning, published in 1995, into a format that a program called a proof assistant can check mechanically, without taking anything for granted. Unlike recent AI work on the Riemann hypothesis, which sought entirely new mathematics, the goal here was verification: confirming that every logical link in an already-known chain is correct.
What Happened
Tianyi Peng, an Anthropic researcher whose group at Columbia University develops AI-based formalization tools, decided to test whether Claude could make progress on formalizing Fermat’s Last Theorem. The result exceeded expectations: in 11 days, working largely autonomously, Claude produced the first end-to-end, computer-verified proof of the entire theorem.
In the process, Claude wrote 13 million lines of Lean code and generated verifiable proofs of 30,300 intermediate theorems, of which 29,500 ended up forming part of the final proof. Dozens of Claude agents collaborated to define mathematical concepts, prove intermediate theorems, and use them as building blocks for increasingly difficult statements.
Anthropic shared the resulting proof with Kevin Buzzard, a mathematician at Imperial College London who has led a community effort since 2024 to formalize this same theorem in Lean. His reaction was emphatic: he called the achievement extraordinary and noted that the proof assumes nothing beyond the axioms of mathematics, and that along the way it self-formalizes algebra, harmonic analysis, geometry, and number theory.
Context and History
For more than 350 years, entire generations of mathematicians searched for a proof of the theorem, marvelous or not. In 1908, a prize of 100,000 German gold marks (the equivalent of 1 to 2 million dollars today) was announced for anyone who could prove it, and in the first year alone, 621 incorrect attempts were submitted.
In June 1993, Andrew Wiles presented what he believed was the first correct proof, in a series of three lectures. Two months later, amid an intensive review, a referee asked him a question that exposed a critical gap in the argument. Wiles spent a year trying to fix it, first alone and then together with his former student Richard Taylor. He came close to abandoning the project until he realized that an approach he had previously discarded could solve the problem. The corrected proof was published in May 1995 and relied on techniques far more advanced than Fermat’s time, which is why today it’s believed that Fermat’s original marvelous proof was, in fact, incorrect.
A decade later, Dutch computer scientist Jan Bergstra proposed formalizing Wiles’s proof. Since then, mathematicians have been developing the methods needed to encode such a complex proof, including the multi-year community effort that Kevin Buzzard launched in 2024 to complete the formalization using the Lean proof assistant. The blueprint alone (the plan describing the project’s initial phase) runs 86 pages.
Technical Details and Performance
A proof assistant like Lean algorithmically verifies the logic of a proof, demonstrating its correctness beyond any doubt. The hard part for humans is rewriting the proof so that Lean can understand it: while a proof meant for human readers skips obvious steps, Lean needs to see every step, no matter how trivial it seems. Moreover, a human proof draws on centuries of published work, while a formalization starts from the tiny fraction of mathematics that has already been formalized.
To put the achievement in perspective: formalizing Fermat’s Last Theorem was expected to take years. Claude did it in 11 days, with 13 million lines of Lean, more than five times the size of Mathlib, the community proof library this proof is built on. Claude’s proof follows a simplified version of Wiles’s argument based on the work of Darmon, Diamond, and Taylor. According to Anthropic, human mathematical input was limited to occasional interventions, not guiding every step of the process.
| Aspect | Wiles’s Proof (1995) | Claude’s Formalization (2026) |
|---|---|---|
| Format | 129 pages on paper, for human readers | 13 million lines of Lean code |
| Verification | Manual review by mathematicians over months | Automatic verification by the Lean kernel |
| From presentation to publication | From June 1993 to May 1995, after fixing a critical gap | 11 days of work, largely autonomous |
| Required level of detail | Skips steps a mathematician takes for granted | Every step, no matter how trivial, must be made explicit |
💭 Key point: Claude didn’t discover new mathematics: it verified that Wiles’s proof, adapted by Darmon, Diamond, and Taylor, is logically correct down to the level of the axioms.
How to Start Trying It Out
You don’t need to be a professional mathematician to try a proof assistant like Lean. The standard entry point is elan, Lean’s version manager, available on Linux, macOS, and Windows.
On Linux and macOS:
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elan --versionOn Windows (PowerShell):
Invoke-WebRequest -Uri "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -UseBasicParsing | Invoke-Expression
elan --versionWith Lean installed, a first trivial example verifies that addition is commutative:
theorem suma_conmutativa (a b : Nat) : a + b = b + a := by
ringThis block defines a theorem and proves it with the ring tactic, which automatically resolves algebraic equalities. An example closer to the spirit of the Fermat project is to state the theorem as a general proposition, the way it appears in Mathlib before having a proof:
def UltimoTeoremaFermatPara (n : Nat) : Prop :=
∀ a b c : Nat, 0 < a → 0 < b → 0 < c → a ^ n + b ^ n ≠ c ^ n
theorem ultimo_teorema_fermat : ∀ n : Nat, 2 < n → UltimoTeoremaFermatPara n := by
sorry -- this is where Claude's 13 million lines came inThe keyword sorry tells Lean trust me, this is true, and it’s exactly what a formalization project has to eliminate completely. To confirm that a finished proof doesn’t rely on shortcuts or unwanted axioms, Lean offers a direct verification command:
#print axioms ultimo_teorema_fermat💡 Tip: run#print axioms theorem_nameon any proof in Lean and check that only the expected axioms of set theory appear: ifsorryAxshows up, the proof still has gaps.
Impact and Analysis
The value of this work isn’t in solving an open problem, but in demonstrating that automatic verification can scale to proofs spanning hundreds of pages written by humans. Understanding a new mathematical result well enough to trust its correctness can take months or years of peer review work. Kevin Buzzard noted that AI self-formalization artifacts are now robust enough to build on, something that wasn’t obvious until recently.
The honest limitation is that this approach doesn’t generate new mathematics on its own: it needs an already-published human proof to translate. It also doesn’t eliminate the need for trust, it just shifts it: instead of trusting hundreds of human reviewers, you have to trust the Lean kernel and its axioms, a much smaller and more auditable piece of software. And a 13-million-line proof, while verifiable step by step, is still enormous for a human to read from start to finish.
What’s Next
If formalizing a proof of this magnitude went from an estimated years to just 11 days, the bottleneck for verifying important mathematical results might no longer be human reviewers’ time. Buzzard suggested that this advance is a significant step toward a future in which all of mathematics can be easily checked, and that as AI produces more proofs, the ability to formalize them quickly could ease the burden of evaluating new results.
📖 Summary on Telegram: View summary
Try it yourself: install elan, clone the Mathlib repository, and run #print axioms on your own lemma to watch the Lean kernel verify your first step today.
Frequently Asked Questions
What Is Fermat’s Last Theorem?
It’s the claim, written by Pierre de Fermat in 1637, that there are no positive integers a, b, and c that satisfy a^n + b^n = c^n for any n greater than 2. Andrew Wiles published the first accepted proof in 1995.
What Does It Mean to Formalize a Mathematical Proof?
It means rewriting the reasoning in a language that a proof assistant, like Lean, can verify mechanically, without skipping any step, no matter how obvious it seems to a human reader.
Did Claude Discover New Mathematics With This Work?
No. Claude verified an already existing proof, Andrew Wiles’s, simplified according to Darmon, Diamond, and Taylor. The achievement lies in the scale and speed of the verification, not in a novel mathematical result.
How Much Lean Code Did Claude Write?
13 million lines, generating verifiable proofs of 30,300 intermediate theorems, of which 29,500 were used in the final proof.
Why Does Kevin Buzzard’s Opinion Matter?
Buzzard has led the community effort to formalize Fermat’s Last Theorem in Lean since 2024, with an 86-page blueprint. His validation confirms that Claude’s result is consistent with that reference project.
Can the Formalization Work Be Reviewed?
Anthropic’s original announcement describes the process and shares Buzzard’s reaction; to understand how a formalization of this kind is built, you can explore the Lean and Mathlib code and documentation directly.
References
- Formalizing Fermat’s Last Theorem: Anthropic’s original announcement, with the project timeline and Kevin Buzzard’s quote.
- Mathlib4 on GitHub: the community library of Lean proofs on which the formalization was built.
- Official Lean Documentation: reference for the language and proof assistant used in the project.
- Fermat’s Last Theorem on Wikipedia: full historical context, including Andrew Wiles’s proof.
📱 Enjoy this content? Follow @programacion on Telegram for daily tech content in Spanish: quick summaries, fresh content every day.
Imagen destacada: Foto de Vitaly Gariev en Unsplash
0 Comments