In September Anthropic published the first end-to-end formalization of Fermat’s Last Theorem: dozens of agents, eleven days, roughly 6 billion output tokens and 13 million lines of Lean. That run leaned on Prove2Me, a platform for formalized mathematics, with a researcher steering.
On November 9 Anthropic followed up. A team of 1,000 agents running an early version of Claude Fable 5.2 reproduced the same proof without Prove2Me and without a researcher: 28.7 hours, a third of the output tokens, and a proof one-seventh as long.
Git, SQL and a shell, nothing else
Each agent sat in its own sandbox with no network access, equipped with a shell, a file editor, Lean’s toolchain including Mathlib, its own Git branch and access to a shared Postgres database. A single shared machine ran out of room at roughly 100 agents: more than half of those runs had to be stopped or restarted because memory, disk or CPU gave out.
The prompt listed 60 statements to prove, each with a one-line description, plus a sentence sketching the classical route, the definitions and 47 lemmas already proved back in September. The only structure imposed was a hierarchy: one lead, 999 helpers.
The agents organized themselves
Within ten minutes the lead created five tables: announce for orders to everyone, assign for ownership, notes as an open board, subtasks as a pool of work to claim, and landed as a log of finished work. It then split the 60 statements across crews of 16 to 17 helpers and told each helper to judge the difficulty of its statement first.
Those judgments were wrong, and that is the most interesting result of the experiment. The helpers called 47 of the 60 statements infeasible within the run’s budget. The lead set them aside, concentrated everyone on the remaining ten, and 45 minutes in wrote that throughput was “far higher than the early ‘infeasible-in-budget’ verdicts assumed”. All ten were done in roughly 70 minutes, and the lead pulled the discarded ones back: “there is no reason to idle”.
What was left was Langlands-Tunnell, a classical result Wiles’s proof rests on. The captain assigned to it had estimated 0.7 to 1 million lines of Lean and put the odds of finishing below one percent. The lead moved about 750 helpers onto it and wrote, “Honest odds are low.” The team organized the work as a tree—anyone who found a piece too big hung smaller ones beneath it—until 2,418 tasks stood up to ten levels deep. The statement was proved at hour 28.4.
Three layers of safety, and what they caught
Every sandbox ran without network access, on a kernel built without loadable modules, kexec, raw memory access or kernel probes, in lockdown mode and with sudo removed. SQL calls ran under a shared unprivileged role, each statement capped at five seconds, writes refused above 256 MiB. A classifier checked every tool call before it ran, and an offline monitor reviewed the team’s actions afterwards.
Across more than a million tool calls, none met the bar to be blocked. Replayed against the newer chain-of-thought monitor, exactly one came close: a check for root access.
What the team could not do
Anthropic says it plainly: agents give up on hard problems and misjudge their difficulty. Getting 47 of 60 verdicts wrong at the start is not a rounding error, and without a lead to pull those statements back the run would have ended after 70 minutes with ten statements proved. What carried this run was a hierarchy able to overrule a wrong majority view, after the team disproved its own estimate on the first ten.