Claude Formalizes Fermat’s Last Theorem in Lean in 11 Days
Fermat’s Last Theorem has been mathematically proven for more than 30 years. So why is an AI system proving it again?
The answer is formal verification.
Anthropic reports that Claude completed a full machine-checkable formalization of Fermat’s Last Theorem in Lean in just 11 days, generating approximately 13 million lines of Lean code and proving more than 30,000 intermediate theorems along the way.
The project did not discover a new mathematical proof of Fermat’s Last Theorem. Instead, Claude translated an established proof strategy into a formal language that a computer can verify step by step.
The complete repository is available on GitHub:
https://github.com/anthropics/fermats-last-theorem
The significance of the project is therefore less about replacing Andrew Wiles’s mathematics and more about demonstrating how AI agents can transform complicated human mathematics into machine-verified formal mathematics at large scale.
🧮 Why Formalize Fermat’s Last Theorem Again? #
Fermat’s Last Theorem states that for integers (n > 2), there are no positive integers (a), (b), and (c) satisfying:
$$ [ a^n + b^n = c^n ] $$
Pierre de Fermat famously wrote the claim in the margin of his copy of Arithmetica around 1637, adding that he had discovered a remarkable proof but that the margin was too small to contain it.
That alleged proof remained undiscovered.
More than three centuries later, Andrew Wiles announced a proof in 1993. A flaw was subsequently discovered, and Wiles worked with Richard Taylor to repair the argument.
The corrected proof was eventually published in 1995.
Fermat’s Last Theorem was therefore already mathematically established.
But traditional mathematical proof and formal proof verification are fundamentally different.
A conventional paper can write:
By Theorem X, the required property follows immediately.
A formal proof must provide enough information for a proof assistant to verify exactly why the conclusion follows.
Definitions, assumptions, intermediate lemmas, type information, and logical dependencies all have to be represented explicitly.
The distinction can be summarized as:
Human Mathematics
│
▼
Natural-Language Proof
│
▼
Human Peer Review
│
▼
Mathematical Acceptance
versus:
Formal Mathematics
│
▼
Lean Code
│
▼
Proof Assistant
│
▼
Kernel Verification
Formalization therefore provides a different kind of confidence: the final artifact can be checked mechanically according to precisely defined logical rules.
📜 From Wiles to Machine-Checked Mathematics #
Wiles’s proof is famous not only because it solved Fermat’s Last Theorem, but also because it connects several deep areas of modern mathematics.
The formalization path used by Claude follows an established route built on Wiles’s work and associated results.
It involves concepts from areas including:
- Number theory
- Algebra
- Algebraic geometry
- Modular forms
- Elliptic curves
- Galois representations
- Harmonic analysis
This complexity explains why formalizing the proof is such a substantial engineering task.
A human mathematician can understand a high-level argument and rely on years of accumulated mathematical knowledge.
A proof assistant cannot simply assume that background knowledge.
Every required result has to exist in a form the system can use.
Formalization therefore becomes a combination of mathematics, software engineering, dependency management, and automated theorem proving.
🤖 11 Days, 30,000+ Theorems, and 13 Million Lines #
According to Anthropic’s account, Claude generated formal proofs for approximately 30,300 theorems, with around 29,500 incorporated into the final repository.
The total codebase reached roughly 13 million lines of Lean code.
That number is enormous compared with conventional mathematical writing.
It also reveals an important characteristic of current AI-generated formal mathematics: successful formalization does not necessarily produce elegant or compact code.
A human expert might compress a familiar mathematical argument into a few carefully chosen lemmas.
An AI system may instead generate many intermediate definitions and supporting results.
Conceptually:
Human Proof
│
├── Major Idea
├── Lemma
└── Conclusion
AI-assisted formalization may look more like:
Major Idea
│
├── Definition A
│ ├── Lemma A1
│ ├── Lemma A2
│ └── Lemma A3
│
├── Definition B
│ ├── Lemma B1
│ ├── Lemma B2
│ └── Lemma B3
│
└── Final Construction
├── Lemma C1
├── Lemma C2
└── Theorem
The result can be mechanically correct while remaining substantially more verbose than human-written mathematics.
That is not necessarily a problem.
For formal verification, correctness is the first requirement. Code elegance and maintainability can be optimized afterward.
🧠 Claude Did Not Invent a New Proof #
This distinction is critical.
Claude’s accomplishment should not be described as independently discovering a new proof of Fermat’s Last Theorem.
The theorem was solved by Wiles and Taylor decades ago.
Instead, Claude’s task was to formalize an existing proof strategy in Lean.
The significance lies in the scale and speed of the translation.
Formalizing a major proof requires turning high-level mathematical reasoning into a hierarchy of definitions and machine-checkable lemmas.
For an AI system, this creates a different challenge from ordinary theorem solving:
Understand Existing Mathematics
│
▼
Identify Dependencies
│
▼
Formalize Definitions
│
▼
Prove Intermediate Lemmas
│
▼
Connect Major Theorems
│
▼
Verify Final Statement
The system therefore has to maintain consistency across thousands of interconnected pieces.
🕸️ How Multiple Claude Agents Worked Together #
One of the project’s most interesting technical aspects was its use of multiple agents.
Early experiments reportedly exposed a major problem: individual agents could prove local results but struggled to maintain a reliable global understanding of a massive proof project.
An agent might solve one lemma without knowing:
- Whether another agent had already proved it
- Which version was canonical
- What downstream theorem depended on it
- Where the result belonged in the overall proof
- How to recover after a failed long-running task
The solution was to introduce structured task orchestration.
🔗 Prove2Me Turns Mathematics Into a Dependency Graph #
The Prove2Me platform organizes formalization work as a directed acyclic graph (DAG).
Each node represents a mathematical task, while edges represent dependencies.
A simplified version looks like:
Final Theorem
▲
│
Major Theorem
▲ ▲
│ │
Lemma A Lemma B
▲ ▲ ▲ ▲
│ │ │ │
A1 A2 B1 B2
This structure gives agents a clearer understanding of what they should work on next.
Instead of asking an AI system to “prove Fermat’s Last Theorem,” the project can decompose the objective into thousands of bounded tasks.
Agents then work on individual nodes while the dependency system connects their results.
This is an important lesson for AI research:
Model intelligence is only one part of solving long-horizon problems.
The surrounding architecture matters too.
🏗️ AI Scaffolding May Matter as Much as Model Intelligence #
A single language model has limited context and cannot reliably maintain every detail of a multi-million-line project in its working memory.
External scaffolding changes the problem.
The system can provide:
- Persistent state
- Dependency tracking
- Task decomposition
- Result retrieval
- Parallel execution
- Compilation feedback
- Failure recovery
- Natural-language theorem descriptions
This transforms a large mathematical problem into a collection of manageable engineering tasks.
The resulting workflow resembles distributed software development:
Global Mathematical Goal
│
Dependency DAG
│
┌───────────────┼───────────────┐
▼ ▼ ▼
Agent A Agent B Agent C
│ │ │
▼ ▼ ▼
Lemmas Proofs Definitions
│ │ │
└───────────────┼───────────────┘
▼
Lean Compiler
│
▼
Verified Artifacts
This architecture could ultimately prove more broadly useful than the Fermat project itself.
The same approach can potentially be applied to formalizing other large mathematical theories and verifying complicated arguments.
🔍 Who Actually Verifies the AI’s Proof? #
This is where Lean becomes particularly important.
Claude generates the proof code.
Lean’s kernel checks it.
That distinction prevents the AI system from simply declaring that its answer is correct.
A successful formal proof must satisfy the proof assistant’s logical requirements.
In other words:
Claude
│
│ generates
▼
Lean Proof
│
│ checked by
▼
Lean Kernel
│
▼
Accepted / Rejected
If the generated proof contains an invalid inference, missing assumption, incompatible type, or other logical problem, the formal checker rejects it.
This provides an important verification boundary for AI-generated mathematics.
The model can make mistakes.
The formal system does not simply trust the model’s assertion that the mathematics is correct.
🧪 Formal Verification Does Not Replace Mathematical Understanding #
There is an important limitation.
A proof assistant can establish that a formal proof follows from its formal foundations.
It does not automatically explain why the proof is mathematically insightful.
Consider two proofs:
Proof A
Short, elegant, conceptually illuminating
and:
Proof B
Correct, enormous, mechanically generated
A formal system can verify Proof B.
A mathematician may still prefer Proof A for understanding.
This distinction becomes increasingly important when AI-generated formal proofs become extremely large.
A 13-million-line proof can provide machine-level verification while remaining difficult for humans to read.
The future of mathematical AI may therefore require two complementary artifacts:
Human-Facing Proof
→ Intuition
→ Strategy
→ Mathematical Significance
→ Conceptual Explanation
Machine-Facing Proof
→ Definitions
→ Dependencies
→ Formal Logic
→ Kernel Verification
The two representations serve different purposes.
📚 Why This Could Change Mathematical Peer Review #
Traditional mathematical review has a scaling problem.
As mathematical arguments become more complicated, verifying every dependency manually becomes increasingly difficult.
Researchers routinely rely on established theorems and omit intermediate steps that experts consider routine.
That is normal mathematical practice.
But when a proof crosses multiple mathematical domains, tracing every dependency can become a substantial undertaking.
Formalization offers a complementary approach.
Instead of requiring every reviewer to manually verify every logical transition, researchers can provide a machine-checkable formal artifact alongside the conventional paper.
The workflow could eventually look like:
Research Paper
│
├── Human-readable proof
│
└── Formal Lean proof
│
▼
Proof Checker
│
▼
Machine Verification
Human researchers could then spend more time evaluating the theorem’s conceptual contribution rather than manually checking every low-level inference.
🌎 AI Formalization Is Moving Beyond Huge Labs #
The Fermat project also points toward a potentially important change in accessibility.
Anthropic reportedly conducted another experiment in which researchers used three personal Claude Max accounts, working through Prove2Me, to formalize Vinogradov’s three-primes theorem in three days.
The broader implication is that large-scale formalization may not always require a massive dedicated research organization.
If the right combination of:
- Capable language models
- Proof assistants
- Mathematical libraries
- Task decomposition
- Persistent project state
- Multi-agent coordination
is available, relatively small teams may be able to tackle formalization projects that once required years of specialized labor.
The bottleneck may gradually shift from writing every proof manually toward designing effective mathematical automation systems.
📈 What This Means for AI Mathematics #
The Fermat project does not demonstrate that AI has surpassed mathematicians.
It demonstrates something more specific—and potentially more practical.
AI systems are becoming increasingly capable of operating inside formal mathematical environments.
That creates several potential applications.
Automated Proof Formalization #
Existing mathematical literature could increasingly be translated into formal proof systems.
This could make previously informal mathematical knowledge easier to verify computationally.
AI-Assisted Proof Checking #
Models could help identify missing assumptions, ambiguous arguments, or gaps in formalization before human researchers invest substantial time reviewing them.
Machine-Verified AI Mathematics #
Future AI systems could generate mathematical conjectures and proofs while proof assistants independently validate the formal results.
Large-Scale Mathematical Engineering #
Complex formalization projects could increasingly resemble software engineering projects, with automated agents handling individual components while humans design the overall architecture.
🧩 The Real Achievement Is the Workflow #
It is tempting to focus on the headline:
“Claude proved Fermat’s Last Theorem.”
But that description misses the more interesting technical story.
Fermat’s Last Theorem was already solved.
The important achievement is that an AI system reportedly helped convert a highly complex existing mathematical argument into a machine-checkable formal artifact at enormous scale.
The project combines:
Large Language Models
+
Proof Assistants
+
Mathematical Libraries
+
Multi-Agent Systems
+
Dependency Graphs
+
Automated Verification
Together, these components create something closer to an AI mathematical engineering platform than a conventional chatbot.
That distinction could become increasingly important as researchers attempt to formalize much larger bodies of mathematics.
🏁 Conclusion #
Claude did not discover Fermat’s Last Theorem, and the theorem itself has not suddenly become an open problem again.
What changed is the way the proof can be produced and verified.
According to Anthropic, Claude completed a large-scale Lean formalization in 11 days, generating around 13 million lines of code and tens of thousands of verified theorems.
The project demonstrates that AI agents can participate in mathematical work far beyond generating plausible-looking equations or explanations.
More importantly, the combination of AI models with formal proof assistants creates a powerful division of labor:
AI generates and organizes mathematical reasoning.
Humans provide mathematical direction and judgment.
Formal systems verify the resulting logical artifacts.
That model may ultimately prove more consequential than the Fermat formalization itself.
The future of AI mathematics may not be about asking a single model to solve an entire theorem from scratch.
It may instead look like a distributed research system in which dozens or hundreds of specialized agents work through a persistent mathematical dependency graph, continuously producing artifacts that a formal verifier can independently check.
Fermat’s Last Theorem was solved by humans more than three decades ago.
What Claude is helping demonstrate now is something different:
How AI can turn monumental human mathematics into software that machines can verify.