Anthropic claims to have created the first fully computer-verified proof of Fermat’s Last Theorem. Dozens of agents from the AI model Claude worked largely independently for eleven days, generating 13 million lines of code in the proof language Lean 4. Mathematicians had estimated that a complete verification of Andrew Wiles’ original proof from 1995 would take several years.
Prove2Me coordinates dozens of agents for the proof
For the work, Anthropic deployed numerous instances of Claude on the open platform Prove2Me. The platform, developed by Anthropic researcher Tianyi Peng at Columbia University, manages thousands of individual theorems as a directed graph and assigns them to individual agents. Fermat’s Last Theorem was deliberately used as a stress test because no known mathematical proof of this magnitude had been fully machine-verified before. Previous attempts with multiple concurrently working agents failed because the systems lost track of already proven intermediate steps.
Each proof step submitted by an agent had to pass the Lean compiler according to Anthropic before Prove2Me marked it as completed in the graph and allowed further agents to build upon it. This built-in verification mechanism prevented errors from individual agents from propagating unnoticed over thousands of intermediate steps.
The finished version consists of 13 million lines of Lean code and includes 29,500 of the total 30,300 generated intermediate theorems. The agents consumed around six billion output tokens over the course of eleven days. Human participants provided the systems with only rough, overarching instructions. The rest was handled independently by the agents.
Proof follows simplified version of Wiles’ argument
The proof does not follow the original 129-page document by Andrew Wiles but rather a simplified presentation by mathematicians Henri Darmon, Fred Diamond, and Richard Taylor. At its core is the modularity theorem, which Wiles proved together with Richard Taylor to solve Fermat’s Last Theorem. The formalization covers prime number exponents starting from the value of seventeen.
Wiles first presented his proof in 1993 but had to close a gap that he and Taylor only fully resolved in 1995. To this day, the manual verification of the argument was considered so labor-intensive that only a few specialists had traced the entire proof in detail.
For the remaining odd prime numbers, the agents relied on existing building blocks from the Lean library Mathlib. The Lean compiler verified the entire result solely based on the three standard axioms of mathematics, without additional assumptions. According to Anthropic, this makes the proof about five times longer than a human-optimized version would be. Brevity was not a goal for the agents, only machine verifiability mattered.
Independent mathematician confirms correctness
Mathematician Kevin Buzzard from Imperial College London, who has been shaping the Lean community for years, confirms the correctness of the formalization. The proof requires no additional assumptions beyond the basic axioms of mathematics and spans algebra, harmonic analysis, geometry, and number theory.
Buzzard sees this as a step towards the automatic formalization of larger parts of the mathematical literature. This could help uncover errors in existing proofs, reduce the workload for reviewers, and make AI-generated mathematics rigorously verifiable in the first place. Similar progress had previously been hinted at by OpenAI’s Astra model, which solved ten unsolved math problems, as well as a proof attempt by GPT-5.6 Sol Ultra for a graph theory conjecture. Both results, however, have not yet been fully independently verified.
As SiliconANGLE reports independently, the sheer processing time of eleven days for a project experts had previously estimated would take several years counts as remarkably short. Anthropic published the complete source code on GitHub and announced discounted access and research grants for external mathematicians who want to keep working with Prove2Me. The exact token and compute cost has not been independently verified and comes solely from Anthropic’s own statements.
What will matter is whether the approach can be transferred to still-unresolved conjectures rather than only retracing already known proofs. So far, the project mainly shows that agent systems can independently split up branching proof work and sustain it over weeks without human intervention. Whether this leads to genuine mathematical discoveries rather than pure formalization of already proven theorems in the foreseeable future remains open.
