Anthropic says its Claude AI has completed a massive formalization of Fermat’s Last Theorem, turning Andrew Wiles’ famous proof into a version that can be verified line by line by a computer. The project reportedly took 11 days, involved dozens of AI agents and produced roughly 13 million lines of formal mathematical code.
In brief
- Anthropic says Claude formally verified Fermat’s Last Theorem in about 11 days.
- The resulting proof contains approximately 13 million lines of code, making it extraordinarily large by mathematical standards.
- Mathematician Kevin Buzzard, who is leading a separate human effort to formalize the theorem, reviewed the work and said it establishes the result using only mathematical axioms.
- The achievement represents formalization of existing mathematics, rather than the discovery of a new proof of the theorem.
A 350-Year Mathematical Mystery Gets a Computer-Checked Version
Fermat’s Last Theorem is one of mathematics’ most famous problems.
The theorem states that there are no positive integers , , and that satisfy:
aⁿ + bⁿ = cⁿ
when the integer exponent is greater than 2.
French mathematician Pierre de Fermat wrote the claim in the margin of a book in the 17th century, famously suggesting that he had found a remarkable proof but that the margin was too small to contain it.
Whether Fermat actually possessed a valid proof became a centuries-long mystery.
The problem was finally solved in the 1990s when British mathematician Andrew Wiles produced a proof using sophisticated mathematical ideas that were developed long after Fermat’s lifetime.
Claude’s achievement is different.
Rather than discovering another way to prove the theorem, Anthropic says its AI system converted the existing mathematics into a formal proof that a computer can independently verify.
Proving Mathematics and Verifying It Are Different Challenges
A conventional mathematical proof depends on a chain of logical arguments that human experts must examine.
Even a correct proof can contain a subtle gap, and finding such an error may require another mathematician to spend months or years examining the work.
Formal mathematics approaches the problem differently.
A proof is translated into an extremely precise computer language, allowing a proof assistant to check whether every individual step follows from previously established definitions, assumptions and theorems.
The approach removes much of the ambiguity involved in human interpretation.
That distinction became especially important with Fermat’s Last Theorem. Wiles initially presented his solution in 1993, but mathematicians later discovered a problem in part of the argument.
Wiles worked with Richard Taylor to repair the gap before publishing the corrected proof in 1995.
The final argument ran to roughly 129 pages and relied on mathematical concepts that did not exist during Fermat’s lifetime.
Humans Were Already Trying to Formalize Wiles’ Proof
Claude’s achievement also overlaps with an ongoing human-led effort.
In 2024, Imperial College London mathematician Kevin Buzzard launched a project aimed at translating Wiles’ proof of Fermat’s Last Theorem into Lean, a formal programming language and proof assistant capable of checking mathematical arguments mechanically.
The undertaking was expected to require years of work and a large community of mathematicians.
Anthropic says Claude completed the formalization in approximately 11 days, dramatically compressing a project that would otherwise involve extensive human effort.
Buzzard subsequently reviewed Claude’s work and reportedly concluded that the formalized proof establishes Fermat’s Last Theorem without relying on assumptions beyond the underlying axioms of mathematics.
Claude Used Many AI Agents Working Together
Anthropic says the project was not completed by a single AI process working continuously from beginning to end.
Instead, researchers used multiple Claude agents operating in parallel.
The agents were assigned mathematical tasks such as creating definitions, proving intermediate results and combining smaller results into increasingly complex arguments.
Human involvement was reportedly limited largely to steering the system toward important unfinished theorems.
The process initially encountered significant problems.
Some agents repeatedly duplicated work, lost track of completed results or failed to coordinate with one another. Anthropic says those early unsuccessful attempts ultimately account for roughly 7% of the lines in the finished proof.
The researchers improved coordination through a tool called Prove2Me, which provided agents with a shared task list and helped organize the formalization process.
The system allowed different agents to see which mathematical problems remained unresolved, reducing duplicated effort and making it easier to build on one another’s results.
30,000 Supporting Theorems and 13 Million Lines
By the end of the project, Claude had reportedly generated more than 30,000 supporting theorems while consuming billions of tokens.
The completed formalization contains approximately 13 million lines of code.
That makes it several times larger than Mathlib, the extensive open-source mathematical library commonly used alongside Lean.
The scale is difficult to visualize.
A typical novel might contain around 80,000 words. By comparison, the formalized Fermat project is equivalent in sheer size to well over a hundred novels worth of machine-readable mathematical logic.
The enormous length does not necessarily mean the underlying mathematics has become more complicated.
Much of the difference comes from the level of precision required when mathematics is written for a computer rather than a human reader.
Claude Did Not Discover a New Proof
The distinction is important.
Claude did not solve Fermat’s Last Theorem for the first time.
Wiles established the theorem more than three decades ago.
Instead, Claude’s contribution was to translate the existing mathematical argument into a format that a computer can verify mechanically.
That could still have major implications for mathematical research.
As mathematicians increasingly produce complex proofs including proofs generated or assisted by AI the ability to automatically verify mathematical arguments could become increasingly valuable.
A computer does not become tired, overlook a line or interpret an ambiguous statement in the same way a human reviewer might.
Formal verification therefore provides something resembling a mathematical audit trail: every step must satisfy the rules encoded in the proof system.
Why Formal Proofs Could Become More Important
The challenge of verifying complicated mathematics is not new.
Some major computer-assisted proofs have required years of scrutiny before mathematicians were comfortable accepting them.
The proof of the Kepler conjecture, for example, relied heavily on computer calculations and required an extensive review process. Grigori Perelman’s proof of the Poincaré conjecture also required substantial time for the mathematical community to fully examine and understand.
AI could dramatically increase the number of mathematical arguments being produced.
That creates a potential bottleneck: if machines can generate proofs faster than humans can verify them, automated formalization becomes increasingly important.
Claude’s Fermat project demonstrates one possible solution.
Instead of asking mathematicians to manually inspect millions of logical steps, a formal proof assistant can mechanically verify whether the argument conforms to its underlying rules.
A Milestone for AI-Assisted Mathematics
The significance of Claude’s achievement therefore goes beyond the famous theorem itself.
Fermat’s Last Theorem had already been solved. What has changed is the ability to take that solution and produce a massive, machine-verifiable representation of it.
Anthropic says the complete formalization has been made publicly available, allowing mathematicians and researchers to inspect and test the work themselves.
If the approach scales to other areas of mathematics, AI systems could increasingly serve not only as tools for discovering mathematical arguments, but also as systems for translating, organizing and formally verifying them.
The remarkable part of the project may ultimately be less about proving a 350-year-old theorem and more about demonstrating how AI and formal proof systems could change the way mathematics is written, checked and trusted.
