Anthropic's Internal Model Formalizes Fermat's Last Theorem in Lean in 11 Days

Anthropic published a research note on Sept. 4 describing an internal model that formalized Fermat's Last Theorem in the Lean proof assistant, start to finish, in eleven days ¹. The run began on Aug. 7 and ended on Aug. 18. It produced roughly 6 billion output tokens, 13 million lines of Lean, and 29,500 intermediate theorems ¹. The whole structure compiles under Lean's kernel, with the axioms of mathematics as its only assumptions ¹. Kevin Buzzard reviewed the result and put his name to it ¹. He is the Imperial College mathematician who has led the human effort to formalize the same proof since 2024. Anthropic describes the model as roughly comparable to Claude Fable 5.1, which it released to the public three days earlier.

Why does a proof of a theorem Andrew Wiles settled in 1995 belong on a ledger about superintelligence? Because the ledger's definition asks for unsupervised work that runs for weeks on tasks experts find hard. This run is the longest single autonomous mathematical job on the public record. The question is how much of a step it earns.

Lean's kernel checked every step of the model's proof

Formalization is translation under a strict grader. A human proof of Fermat's Last Theorem runs through modularity lifting, Galois representations and a great deal of algebraic number theory. Mathematicians accept much of it on trust in one another. Lean demands each step in full. Every step has to reduce to earlier steps until the chain reaches the axioms, and the kernel either compiles the whole thing or it rejects it ¹.

That grader is the reason the result carries weight on this ledger. A benchmark score arrives from the vendor's own harness, and independent boards have disagreed with vendor harnesses by fifteen to thirty points across the summer. Here the checker ships with the proof. Anthropic states that a human set the goal and the environment, and the proof assistant was the only judge along the way ¹.

Buzzard's role matters for the same reason. His team spent two years building the Lean infrastructure for the proof. He is the person best placed to say whether the model's 29,500 lemmas amount to the theorem or to a pile of technicalities that dodge it. "This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," Buzzard said in the note ¹. Read the sentence for its hedge. Eleven days is Anthropic's number, and Buzzard marks it as such. The proof itself he vouches for outright.

The case for the move

Buzzard's sentence is the strongest case that the reading should move up. A research-grade proof, fully checked, in eleven days, is a long-horizon result. Static benchmarks stopped measuring that kind of work once frontier models cleared them. An outsider verified this one, which is the bar the method sets for the higher steps.

Three features of the run push toward a larger step. Eleven days of continuous work is a horizon well past anything the public time-horizon measurements have recorded for a single task. A program checked the output, in place of a vendor grading it. Human experts had already invested two years on the same target, which gives the comparison a real baseline.

The case for a smaller step

Three reasons shrink the step.

First, the mathematics was known. Wiles published in 1995, Buzzard's group had mapped much of the route into Lean, and the model's job was to close the remaining distance under a checker. That is a hard translation task and a long one. Finding a theorem is a different thing. The definition's first clause asks for economically valuable work across occupations, and formalizing a settled proof is one narrow instance of it.

Second, the model is internal. Anthropic describes it as comparable to Fable 5.1, and only Anthropic has run it. A result from a system the public can use would earn a confirmed step. One from a system only the vendor has run earns a reported one, whatever the checker says about the output.

Third, the forecasting record moved the other way over the same months. Daniel Kokotajlo wrote AI 2027, the fastest widely read timeline of 2025, and he said this year that the field is running behind it ². "Things seem to be going somewhat slower than the AI 2027 scenario," Kokotajlo said ². He put a number on the revision in a later interview. "Our timelines were longer than 2027 when we published and now they are a bit longer still," he said, adding that around 2030 is what he now tells people, with a great deal of uncertainty ³. So Kokotajlo lengthened his scenario while machine proofs got longer. That pairing is the tell. Capability results of this kind were already priced into his 2027 story. The rest of the story, the part about systems automating research at scale, has arrived slower than he wrote it.

Gary Marcus makes the sharper version of the same argument. Writing in July about a panel he shared with three other researchers, he said: "None of the four of us believe that LLMs on their own are sufficient for AGI" ⁴. A Lean proof from a language model answers part of that claim, since the proof is real and the model produced it. It leaves the rest standing. Eleven days of formalization say little about reliability on open-ended work where the grader is missing.

Where this sits on the ledger

The reading measures four clauses: unsupervised expert work across occupations, ten gigawatts acting as one machine, measured self-improvement, and third-party proof of execution. This result touches the first clause and, in a small way, the fourth, since a Lean kernel is a form of proof of what ran. It leaves the compute clause untouched. Self-improvement stays untouched too, because the model formalized mathematics instead of its own successor.

Epoch AI's trend data gives the scale of the background against which one result lands. Frontier training compute has doubled roughly every 5.2 months since 2020, and Epoch expects the pace to slow from 2026 ⁵. In mid-July, FutureSearch's tracker put the Metaculus community median for general AI at January 2033, with a 25 percent chance by 2029 ⁶. A ledger that moved a full point on every impressive result would have crossed fifty by now. This one moves 0.6, in the capability component, at reported confidence. It will move further on the day an outside team runs a public model against a comparable target and publishes what happened.

By the numbers

• 11 days from Aug. 7 to Aug. 18 for the full formalization run ¹
• Roughly 6 billion output tokens generated across the run ¹
• 13 million lines of Lean and 29,500 intermediate theorems in the finished proof ¹
• Two years of human effort on the same Lean target under Buzzard's group before the run ¹
• 5.2 months per doubling of frontier training compute since 2020, with a slowdown expected from 2026 ⁵
• January 2033 as the Metaculus community median for general AI, with 25 percent by 2029 ⁶
• Around 2030 as Kokotajlo's revised central estimate ³

What to watch

An independent group running a public model against a comparable formalization target, with the run logged, would turn this reported step into a confirmed one. New mathematics, checked the same way, would engage the definition's first clause directly. Kokotajlo's next timeline update is the other marker. So is the first outside measurement of how much frontier research the labs' own agents now perform, which would settle whether the forecasters or the lab notes read the record correctly.