Summary: Anthropic said Claude agents formalized Fermat’s Last Theorem in Lean over 11 days, producing more than 13 million lines that a proof assistant checked. Kevin Buzzard verified the result against standard axioms but said it follows existing literature and adds essentially nothing to mathematics. The case highlights environment engineering and mechanical verification rather than a new mathematical proof.
On September 4, 2026, Anthropic said it had passed a milestone for AI in mathematics: over the course of 11 days, a swarm of Claude agents turned Fermat’s Last Theorem into a complete Lean development that a proof assistant then checked mechanically. Posed in 1637, the problem had to wait until 1995 for Andrew Wiles, whose proof ran to 129 pages. It now exists as more than 13 million lines of code that rest on nothing beyond Lean’s three standard axioms. The proof is published on GitHub, where anyone who wants to can rerun the verification.
The Run in Numbers: Eleven Days, Six Billion Tokens
The theorem says that once n exceeds 2, no three positive integers can satisfy aⁿ＋bⁿ＝cⁿ. Anthropic did not hand the problem to a single model and wait for one finished answer; it split the work across dozens of Claude agents running in parallel. Those agents sat on an internal research model, roughly on a par with Claude Fable 5.1, which put out about six billion output tokens over the 11 days and wrote more than 13 million lines of Lean — over five times the size of Mathlib, Lean’s mathematics library. In total 30,300 theorems were proved, and 29,500 of them feed into the final proof. Rather than reinventing the mathematics, the effort followed the Darmon–Diamond–Taylor 1995 simplification of Wiles’s argument. That scale does not come free: Kevin Buzzard reported that compiling the result took roughly 20 times as long as compiling Mathlib, on a machine with 96 cores and 500 GB of RAM.
Humans Supplied Only the Direction
The project was started by Anthropic researcher Tianyi Peng, whose group at Columbia University builds AI formalization tools. Their creation is Prove2Me, an open collaborative platform that keeps a DAG of theorem dependencies, makes Lean compilation faster, and gives agents a way to search for and reuse results that already exist. Around it sits a multi-agent harness built on Claude Code. Human involvement stayed thin — Peng now and then offered a high-level steer, such as “Jacobian as a scheme sounds high priority.” Nothing went to waste, not even the wrong turns: output from the earliest agent runs accounts for roughly 7% of the non-boilerplate lines in the finished proof. There was a smaller demonstration too, of how accessible this has become — agents on three personal Claude Max plans formalized Vinogradov’s three primes theorem in three days.
Buzzard: The Check Passes, But Mathematics Learns “Essentially Nothing”
Kevin Buzzard of Imperial College London served as the verifier. Since 2024 he has led the community’s FLT formalization effort, funded by a five-year, £1 million EPSRC grant. Buzzard compiled the proof himself and ran a comparator, which confirmed that the statement lines up with Mathlib’s own FLT declaration. It checks out, he concluded, proving the theorem “with no assumptions other than the axioms of mathematics,” through techniques that could help with “rooting out errors in the current mathematical corpus and lightening the load of referees.” He then poured cold water on the mathematical content: the formalization “just faithfully follows the early literature on the proof and adds nothing,” and so tells mathematics “essentially nothing.” To close off the possibility that the AI had exploited soundness bugs in Lean’s checker, he read by hand all of the roughly 100 lines of non-mathematical code — a convenience tactic, nothing more. One side effect: Freek Wiedijk’s list of 100 formalization challenges now stands fully closed. There is also a human detail worth keeping. Buzzard was at a festival in Wales with poor phone reception when the announcement arrived, took it for a crank email, and only caught up a week later. Claude’s own log captured the other half of the moment — “The FLT root reads Proved on the site. Historic moment (modulo re-check).”
Implications for AI Engineering
Three things stand out. First, long-horizon agent work has cleared another reality check: 11 days, dozens of agents, tens of millions of lines. What made it possible was not a bigger model but environment engineering — a compiler that returns an unambiguous success signal, a shared task graph inside Prove2Me, and failed attempts that could be picked back up. Second, formal verification is turning into the next battleground over AI code quality: once “it compiles” carries the same weight as “it is mathematically correct,” review stops being a matter of reading code line by line and becomes a matter of running a proof checker. Third, the economics are starting to add up: community estimates price six billion output tokens in the low hundreds of thousands of dollars at API rates, set against Buzzard’s five-year academic grant. As he wrote, if thousands of pages of literature can now be formalized end to end by an AI swarm in 11 days, formalization of modern research will soon happen on the fly — and it will keep the field honest about results that are merely “known to the experts.”