Fermat's Last Theorem — the statement that the equation xⁿ + yⁿ = zⁿ has no integer solutions for exponents n greater than 2 — resisted mathematicians for more than 350 years after Pierre de Fermat scribbled his famous "margin too small" note around 1640. Andrew Wiles finally proved it in the mid-1990s. Now Anthropic says a swarm of its Claude agents has done something no human team had completed: translated that proof into a form a computer can check line by line.
According to the company, dozens of Claude agents working largely autonomously produced the first complete, machine-verified formalization of Fermat's Last Theorem in the Lean proof assistant — roughly 13 million lines of Lean code containing around 29,500 intermediate theorems. The work took 11 days. Anthropic researcher Tianyi Peng, whose Columbia University group builds AI-assisted formalization tools, oversaw the effort with occasional high-level instructions; the agents handled the rest.
Lean is both a programming language and a verification system. A mathematical claim and its derivation are written as code, which Lean checks against a fixed set of logical rules. If any link in the chain is missing, the proof simply does not compile. That is the point: trust shifts from the diligence of human reviewers to a small, audited logical core.
Several early attempts failed, the company says: initial agent teams made partial progress but lost track of the overall project state and stopped collaborating effectively. The breakthrough came only after a switch to Prove2Me, an open formalization platform developed by Peng and colleagues at Columbia. It maintains a directed acyclic graph of theorem statements, letting agents decide which proofs to tackle next — a design intended to counter memory degradation and enable parallel work.
The scale of the effort is striking. Anthropic says the agent team consumed roughly six billion output tokens, which outside observers estimate implies compute costs between $100,000 and $300,000. A side experiment suggests far smaller budgets can work: using just three private Claude Max subscriptions, agents formalized Vinogradov's three-primes theorem in three days.
The formalization follows a simplified version of Wiles' proof after Darmon, Diamond and Taylor, and the code is public in an Anthropic GitHub repository along with a written walkthrough. Kevin Buzzard, who leads a community project at Imperial College London to formalize Fermat's Last Theorem (a project running since 2024 and funded until September 2029), has reviewed the work. He compiled the code himself and ran the comparison tool; it holds. In his Xena Project blog, Buzzard calls it a big step toward automatic formalization of the modern mathematical literature — while stressing that mathematically it adds nothing new, since the formalization follows the early literature of the proof.
The achievement sits in a mixed recent record for AI in mathematics. In 2024, DeepMind's AlphaProof and AlphaGeometry 2 reached silver-medal level at the International Mathematical Olympiad. In April 2026, a 23-year-old used a single prompt to GPT-5.4 Pro to crack a 60-year-old Erdős problem, a proof later verified in Lean. Shortly afterward, an internal OpenAI reasoning model refuted an 80-year-old conjecture about the planar unit distance problem — though reviewing mathematicians noted the argument leaned on ideas that could, in hindsight, be attributed to other authors.
For formal mathematics, the message is that infrastructure may matter as much as raw model capability: the decisive ingredient in the Fermat formalization appears to have been Prove2Me's planning graph, not a smarter model. For the wider field, a famous theorem's proof being machine-checkable by AI agents in under two weeks — at a cost comparable to a small research grant — reframes what "verifying" a proof means, and how much of the mathematical literature could eventually be placed on a computer-checked footing.
