要点
- On 9 November 2026, Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl, and Lance Martin described a toy experiment on Anthropic's Claude developer blog.
- In September, dozens of agents running an internal model roughly comparable to Claude Fable 5.1 produced the first end-to-end computer-checked formalization of Fermat's Last Theorem, with the Prove2Me platform and direction from a researcher. That run took 11 days, about 6 billion output tokens, and 13 million lines of Lean.
- The new run used 1,000 agents on an early version of Claude Fable 5.2, plus Git and a shared Postgres database. It finished in 28.7 hours.
- Each agent sat in its own sandbox with no internet access. A classifier checked every shell command and file edit. Across more than a million tool calls, none were blocked.
- Helpers first judged 47 of the 60 statements infeasible. The lead later moved about 750 helpers onto Langlands-Tunnell, which a captain had given less than a 1% chance of finishing. The team built a task tree of 2,418 pieces, up to 10 levels deep, and landed the theorem at hour 28.7.
On 9 November 2026, five Anthropic authors posted a detailed account of a toy experiment: 1,000 agents running an early version of Claude Fable 5.2 reproduced a formal proof of Fermat's Last Theorem. The theorem says that no positive integers a, b, and c satisfy a^n + b^n = c^n for any n greater than 2. Andrew Wiles proved it in 1995. Formalizing that proof means rewriting every step in Lean, a language a computer can check. The September formalization, which Anthropic describes as the first end-to-end version, used dozens of agents, an internal model roughly comparable to Claude Fable 5.1, a purpose-built platform called Prove2Me, and steering from a researcher. It took 11 days and about 6 billion output tokens, a measure of how much text the model wrote, and produced 13 million lines of Lean. The new run dropped Prove2Me and the researcher. It finished in 28.7 hours, used one-third as many output tokens, and wrote a proof one-seventh as long. That is a real efficiency result. It is not a story of agents opening a blank file and proving a 350-year-old theorem on their own.
[1][2]What the experiment actually did
The team gave the agents 60 statements to prove, including the final theorem and 59 intermediate milestones. For each statement they also provided a one-line informal description, the definitions those statements use, and 47 lemmas already proved in the September formalization. The prompt included a one-sentence sketch of the classical route through the proof. The only organizational structure in the prompt was a hierarchy: one lead and 999 helpers. The lead was told to split the problem and assign parts. The helpers were told to expect work from the lead and to ask if a task was unclear. During the run, the harness sent the lead 19 automatic reminders of how much time remained, each encouraging it to keep going.
Each agent had a shell and a file editor in its own sandbox, with Lean and the Mathlib mathematics library built into the image, its own Git branch, the ability to open merge requests into main, and access to a shared Postgres database through the shell. A statement counted as proved only when Lean's checker accepted it on the shared main branch.
The authors call this a toy experiment, and they say it does not remove the need for domain-specific platforms. Prove2Me, they note, may still help agents compile Lean faster and reuse human results. The September write-up, which they link, is the prior result this run was asked to reproduce.
[1][2]How the 1,000 agents coordinated
A single shared machine ran out of memory, disk, or CPU at about 100 agents. More than half of those 100-agent runs had to be stopped or restarted. So each of the 1,000 agents sat on its own lightweight virtual machine and coordinated through SQL and Git. The authors chose SQL because transactions can handle concurrent writes, and because Claude already knows how to use it.
In the first 10 minutes, the lead created five tables: Announce, for orders to the whole team; Assign, for who owned each statement; Notes, an open board; Subtasks, a to-do list any helper could claim; and Landed, a log of finished work. It assigned each statement to a crew of 16 to 17 helpers, named a captain for each crew, and told every helper to judge its statement's difficulty.
About 27 minutes in, three statements were already proved. The lead then set aside the 47 statements that most helpers had judged infeasible within the budget and moved nearly all of the helpers onto the remaining 10. Those crews grew to between 46 and 139 helpers. All 10 statements were proved within roughly 70 minutes. The lead wrote that the team's throughput was far higher than the early infeasible verdicts had assumed, then said there was no reason to idle, and began handing the harder statements back out.
Activity later stopped near hour 18, when the authors restarted the run from its last save and gave the agents 12 more hours. By then the remaining mountain was Langlands-Tunnell, a classical result that Wiles's proof relies on, plus the statements that depended on it. The captain of that task had estimated that the proof would take at least 0.7 to 1 million lines of Lean, with less than a 1% chance of finishing on time. The lead moved about 750 helpers onto it and wrote that the honest odds were low.
The first tasks were too large for one helper. The team grew a tree: a piece that was too big could be split, and each piece could assume the pieces beneath it. The tree reached 2,418 tasks and 10 levels. Langlands-Tunnell was proved at hour 28.4, and the final theorem at hour 28.7. The authors' count ends at 54 of 60 statements, because five alternatives were no longer needed and one statement was dropped.
[1][2]What the safety layers did and did not catch
No single layer, the authors write, is enough to contain a team of agents. Each sandbox had no network access. Its only path out was a pipe to a gateway that called the Claude API and forwarded Git and SQL requests. Agents could push only to their own Git branch. Database calls ran under a shared unprivileged role, with a five-second limit on each SQL statement and a refusal of writes above 256 MiB. The gateway tagged each request with the agent's identity outside the sandbox, so one agent could not pose as another. The kernel ran in lockdown mode without features that give a root user a direct path in. Agent commands ran as an unprivileged user, with tools such as sudo removed.
A prompted classifier could block each tool call, including shell commands and file edits. In this run the authors used only the action-based version of that monitor, which sees actions and not the model's chain of thought. A block on the lead would have stopped the whole team. A block on a helper would have removed only that helper. Across more than a million tool calls, none met the bar to be blocked. When the authors later replayed the calls against a chain-of-thought monitor and the current rubric, only one call, a check for root access, came close.
They had tested monitors in separate sabotage evaluations, where red-team agents tried to talk the classifier into permitting a sandbox escape. Monitors that could see chain of thought and messages between agents detected all of those attempts. The authors added that parallel chain-of-thought monitor shortly after this run. They also say they run experiments like this on models that may not have completed Anthropic's pre-release alignment assessment, and that they design the monitoring for the possibility that a model is misaligned.
[1][2]The fair case, and what is missing
The fair reading is that a general-purpose harness (a sandbox, Git, SQL, Lean, and a lead/helper split) was enough to reproduce a known formalization faster and more cheaply than the September setup, once the team was given the milestone list and the already-proved lemmas. That is a genuine result about coordination. Agents that at first refused most of the work later finished it when the lead kept reassigning them, which is also a genuine observation about how these systems misjudge hard tasks.
The gaps sit next to that result. The agents did not choose the 60 statements or the 47 lemmas. They did not invent the classical route. A human-written harness sent the lead 19 nudges to keep going, and the run was restarted at hour 18. The authors do not publish the full traces. The safety claim is that nothing in this run rose to a block, not that the stack would catch every attempt to leave the sandbox. The model itself may not have finished the alignment checks that shipped models receive.
Independent groups cannot yet repeat a 1,000-agent Lean formalization on a publicly specified Fable 5.2 checkpoint and compare token counts and proof length under the same scaffolding.
[1][2]Who should care, and what to watch
Anyone building multi-agent systems for long, decomposable work should care, especially teams deciding whether they need a custom coordination platform or can start with Git and a database. Safety teams should care, because the post is unusually specific about what the monitors saw and what they did not use during the run.
Over the next six months, the checkable items are reproductions and trace releases. Watch whether Anthropic or someone else publishes the task tree, the SQL schemas the lead invented, and a token accounting that another lab can audit. Watch whether a publicly available Fable 5.2 checkpoint, given the same 60 statements and 47 lemmas, finishes in a similar time. Watch whether later write-ups still use only an action-based monitor, or whether the chain-of-thought monitor becomes the default for runs of this size.
[1][2]Close
The experiment shows that a thousand sealed agents, given a shared checklist and a shared database, can rebuild a formal proof that a smaller, more closely directed team had already produced. If later public runs keep the time and token savings under that same scaffolding, general tools will look more sufficient for this class of work than many teams now assume. If the savings shrink once the milestone list or the 47 lemmas are removed, then the September platform and the human decomposition will have been doing more of the work than a casual reading of "1,000 agents proved Fermat" would suggest.
[1][2]