Anthropic says 1,000 agents proved Fermat in 30 hours. The claim has no repository yet

Anthropic's 9 November announcement reduces to a single sentence: a team of 1,000 Claude Fable 5.2 agents, started from minimal prompts, fully formalized Fermat's Last Theorem in 30 hours with minimal human intervention, spending one-third the action tokens of the company's first formalization and returning a proof seven times shorter. If that holds, it is the largest machine-assembled proof anybody has shown in public. Whether it holds is a question about a repository that does not exist yet, and that gap is a better story than the runtime.

The announcement and the engineering post describe different events

The companion post, Safely scaling multi-agent teams with Claude Fable 5.2, went up the same day under Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl and Lance Martin. It calls the work "a new toy experiment" that "reproduced the proof" in 28.7 hours, run on "an early version of Claude Fable 5.2". The system card is more clipped still: "earlier snapshot". Read the three documents in order and the milestone becomes a toy, the leap becomes a reproduction, and the model becomes an earlier version of itself.

That self-description is honest and it is a hedge: a toy experiment on an early snapshot cannot fail in a way that costs anything. The distinction matters because the announcement is not written like a toy: it is written like a result, with a percentage, a token ratio, a length ratio and a wall-clock figure, all the furniture of a benchmark table without the table.

The agents were handed a map and told to walk it

What "minimal prompts" means here is narrower than it reads. Each agent got a list of 60 statements to prove, the theorem plus 59 intermediates, each with a one-line informal description; a single sentence sketching the classical route; the definitions those statements use; 47 lemmas already proved in September; and Lean's Mathlib built into the sandbox image. "We offered no other guidance on how to prove the theorem or organize themselves," the post says. That is accurate about the search, not about the problem, whose decomposition, vocabulary and most of the scaffolding arrived pre-cut.

The September formalization is the reason to take the new number seriously at all, and on every axis except agent count it was the harder job. Dozens of agents on an internal research model roughly comparable to Claude Fable 5.1 on Prove2Me, a platform purpose-built for the task, with direction from Tianyi Peng: 11 days, about 13 million lines of Lean, about 6 billion output tokens. That code is public, and Kevin Buzzard compiled and checked it. The September episode carries an outside signature. This one carries a grader.

One lead, 999 helpers, one Postgres

The architecture is the part of the post worth reading closely. One agent led, 999 assisted. The prompt told the lead to split the problem and assign parts, and told helpers to expect work from the lead. Every agent had a shell, a file editor, its own Git branch with merge requests into main, and a shared Postgres database, all inside its own lightweight VM with no network access; requests left only through a gateway.

SQL carried the coordination because transactions survive concurrent writes from a thousand processes, and Claude already knows how to use it. A single shared machine, by contrast, "hit its limits at about 100 agents: more than half of our 100-agent runs had to be stopped or restarted because memory, disk, or CPU ran out." The harness also sent the lead 19 reminders of remaining time, each encouraging it to keep going.

Safety was enforced by a blocking classifier on every shell command and file edit, fail-closed: a block on the lead ended the run, a block on a helper removed only that helper, and an offline monitor reviewed team actions. After the run Anthropic added a parallel chain-of-thought monitor. Across more than a million tool calls, the company says, none in this run met the bar to be blocked; replayed against the newer monitor and today's rubric, one call came close, a check for root access.

What the kernel checked, and what nobody has

Here the story stops being about model capability, because nobody outside Anthropic can see the Lean code. As of 9 November none of the three documents links a repository, the September repository at anthropics/fermats-last-theorem has not changed since 24 September, and no new repository for this run was found, per the episode breakdown from AI Proved What?. Which leaves the top-level statement, the axioms and the seven-times-shorter claim uncheckable by anyone outside the company. The documents do not say whether length means lines of code or something else, or whether the 47 supplied lemmas count toward the comparison.

Anthropic's grader accepted the proof using only Lean's standard axioms, according to the system card. That is a real bar and it is a narrower one than it sounds. Lean's kernel verifies that a proof follows from a statement; it does not verify that the statement is Fermat's Last Theorem as a mathematician would phrase it. Closing that gap means letting someone read the statement. No independent check is named, no expert reaction was found, and footnote 4 of the announcement says the external organizations it names, its pre-release safety evaluators, did not review the post or the system card. There is no paper. There is no peer review.

The comparison that carries the headline

The contrast with Opus 5.5 is the number doing the persuasive work: same 1,000-agent setup, 26 percent of the formalization in 18 hours, and, in the announcement's phrasing, barely any further progress after 30. Fable 5.2's 86 percent is a weighted share of the 60 statements, scored by Anthropic's own grader, from a single run per model: one sample per arm, an in-house judge.

The system card's smaller-team numbers are less dramatic and more informative: 0.12 against 0.09 for a single agent, 0.35 against 0.21 at 100, with the caveat that Fable 5.2 ran a week later on a shorter brief. Both the brief and the model moved. The team-size curve is the finding; the 26 percent is an anecdote with a decimal point.

A timeline reconstructed from two documents

Three statements were proved by minute 27, and 47 were first judged infeasible. Langlands-Tunnell, the hardest link, took about 750 helpers and a tree of 2,418 tasks, finished at hour 28.4; the final theorem at 28.7. At hour 30, 54 of the 60 statements were proved, five alternatives no longer needed and one dropped. Both runs had an 18-hour budget and were resumed from their last save at hour 18 with 12 more. The blog says no researcher steered the work during the run.

Two things follow. The 30 hours is elapsed time across a checkpoint restart. And "fully formalized" is doing work: 54 of 60, the gap being redundant alternatives and one abandoned case. A reader who trusts the headline will assume all 60 closed cleanly.

What would settle it

Formalization is the one branch of AI research where verification is cheap, mechanical and already built, which makes the missing repository frustrating rather than suspicious: publishing costs a git push. Three artifacts would end the argument. The repository, with the build. The 60 statements written out as Lean declarations, so the top-level theorem can be read. And one outside mathematician with a laptop, compiling it and saying what they think of the statement.

Anthropic has done this before, in September, and that is why this one reads as withholding rather than oversight. Fermat's Last Theorem was proved by Andrew Wiles with Richard Taylor in 1995: nothing here is new mathematics, and the achievement is coordination, not insight. Coordination at this scale is genuinely interesting, and the 1,000-agent claim may well survive contact with a compiler. Until somebody compiles it, what Anthropic has published is a method paper with a benchmark's vocabulary and no benchmark. The headline promises a result that only a repository can deliver.