Claude agents formalize Fermat's Last Theorem in Lean in 11 days

On 4 September, Anthropic published what it calls the first complete computer-checked proof of Fermat's Last Theorem, along with a public Lean repository, and said Claude worked "largely autonomously over 11 days" to produce it. Within hours, Kevin Buzzard of Imperial College London, who has since 2024 led a community effort to formalize the same theorem, pulled the repository, compiled it himself, and ran the standard comparator tool over it. His verdict: "it checks out. It is a gigantic proof (over 13.4 million lines of code)." New Scientist reported the milestone the next day, repeating the 11-day timeline and the 13-million-line scale.

That combination is why this reads as more than a launch post: a first-party artifact, an adversarial recompile by the person best positioned to find the seams, and a byline outlet restating the numbers.

What the build actually is

Formalization means translating a proof written for human mathematicians into a formal language a machine can check line by line, in this case Lean 4. Anthropic states about 13 million lines of Lean, roughly 29,500 intermediate theorems used, and around 6 billion output tokens. The work was assembled on Prove2Me, an open collaborative platform for formalizing mathematics built at Columbia University by Tianyi Peng and his collaborators rather than by Anthropic; Peng is an Anthropic researcher whose Columbia group builds tools for AI formalization. The repository pins the toolchain to Lean 4.33.1 on Mathlib v4.33.0 and ships a FinalCheck axiom guard confirming the proof depends only on three standard axioms: propext, Classical.choice, Quot.sound. A Lean proof that clears that check with no additional axioms and no sorry placeholders is not taking anything on faith beyond the accepted foundations of the library.

What the machine check does not verify is intent. Both Buzzard and the repository's own README stress that semantic review, whether the Lean definitions actually name the mathematical objects a reader thinks they name, stays a human bottleneck. A proof can be logically airtight and still formalize the wrong statement if a definition quietly diverges from its intended meaning. Mathlib, the standard Lean library, requires contributors to disclose LLM use and to understand everything they submit, which is a meaningful bar for an artifact of this size to clear before other formalizations can build on it.

Why the eleven days matter more than the theorem

The theorem was proved by Andrew Wiles in the 1990s, and Buzzard is explicit that the formalization adds essentially no new mathematics. It follows the Darmon, Diamond and Taylor exposition route, not the modern Khare/Taylor-style path his own project targets. As a mathematical result, nothing here is discovery.

As a statement about timelines, it is the whole story. Buzzard's effort has been funded by a five-year EPSRC grant. The premise behind that grant, that formalizing a proof of this depth is a multi-year research program, is the premise an 11-day lab run just contradicted. Anthropic has not disclosed what the run cost, so the direct budget comparison stays illustrative rather than settled; The Next Web could only work list-price token math. But the wall-clock gap is not illustrative. It is 11 days against five years.

That inverts the working assumption behind how this kind of work gets funded and staffed. If autoformalization of published mathematics is now something a lab does in a fortnight rather than something a consortium does across a grant cycle, funders sizing multi-year formalization programs, Mathlib maintainers deciding what enters the library, and journal referees weighing whether a submitted proof arrives already machine-checked are all reasoning from a baseline that no longer holds. The capability on display is conversion, not creativity: turning existing human mathematics into machine-checked form at a pace nobody had priced in. That is narrower than it first sounds, and, for anyone whose plans assumed the old timeline, more disruptive.

Checked, and merely announced

Four days later, OpenAI announced that an unreleased internal model, coordinating what the company said reached 10,000 sub-agents at a compute cost it put in the millions of dollars, had proved finite-time blow-up for the forced Navier-Stokes equations. Terence Tao has characterised the forced version as a stepping stone rather than the full Millennium Prize problem, which concerns the unforced equations. The announcement arrived alongside a credit dispute: NYU's Tristan Buckmaster and Anthropic's Levent Alpöge had published Lean-verified blow-up proofs for several fluid equations hours earlier, and Buckmaster alleged that OpenAI pursued the same narrow technical route after learning of their work, and that he was pressed to drop Alpöge from authorship because Alpöge works for a competitor. OpenAI says neither its researchers nor its agents saw the pair's work before publication and that no user data was accessed; Sébastien Bubeck, who leads OpenAI's math team, called the allegations false and inflammatory.

Set the two announcements side by side and the distinction is not which lab proved more. Anthropic shipped a repository, and the person best placed to attack it compiled it and reported back within hours. OpenAI announced a roughly 100-page proof the field cannot yet check, and the fight that followed was about who deserves credit rather than whether the result holds. Machine-checked is a claim anyone can test. Announced is a claim you have to take.