1,000 agents, 28.7 hours: what Anthropic's Fermat re-run shows

A team of 1,000 agents running an early version of Claude Fable 5.2 produced a computer-checked proof of Fermat’s Last Theorem in 28.7 hours, according to an Anthropic engineering post published on 9 November. The team had one lead and 999 helpers, each in its own virtual machine with no network access. They coordinated through five Postgres tables the lead designed in its first 10 minutes. Three safety layers surrounded the work: a sandbox, a classifier that checked every tool call before it ran and an offline monitor. Anthropic reports that none of more than a million tool calls met the bar for blocking.

The run is a detailed case study in long-horizon agent coordination, but the result is narrower than its shortest summaries. The agents did not start from nothing. They received 60 target statements, a one-sentence sketch of the classical route, the definitions those statements use and 47 proved lemmas from Anthropic’s September formalization. Activity stopped near hour 18, and Anthropic restarted the run from its last save with 12 more hours. Anthropic reports a single run. The new proof has not been released, and no outside party has reported checking it.

This reconstruction rests on Anthropic’s post, Safely scaling multi-agent teams with Claude Fable 5.2, by Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl and Lance Martin. It also draws on the Fable 5.2 launch page, an archived earlier version of that page, the September formalization post and its public repository. Every figure below is Anthropic’s own unless stated otherwise. The Frontier Wire has not run the harness or checked any Lean code.

TL;DR

• One lead agent and 999 helpers proved the final theorem at hour 28.7. They coordinated only through Git and a shared Postgres database, using tables the lead invented.
• The starting kit included 47 proved lemmas from September’s proof, 60 target statements and a proof sketch. Anthropic corrected its launch page on 11 November to describe that kit more accurately.
• Safety was layered: one VM per agent with no network access, an action-only classifier on every tool call and an offline monitor. Anthropic reports no blocks across more than a million calls.
• The bounds: one run, a restart at hour 18, an unpublished proof, no independent check, and an action monitor whose blocking threshold the post does not quantify.

The documents and their dates

The publications in this story were released on different days, and the date of the experiment itself is not given. Keeping them apart matters because one of them changed after release.

What the team was given

The task was to reproduce a proof that already existed in Lean, not to find new mathematics. Anthropic calls it a “toy experiment” in its post. The question it tests is whether general-purpose tools can replace a purpose-built formalization platform and a human director.

Anthropic split the theorem into 60 statements: the final theorem plus 59 intermediate milestones. Each began in Lean with a placeholder for its proof. A statement counted as proved only once Lean’s checker accepted a finished proof, submitted to the shared main branch on Git, where “a grader checked it.” Each statement came with a one-line informal description.

The prompt also included a one-sentence sketch of the classical route, the definitions the statements use and 47 proved lemmas from the September formalization. Lean’s toolchain and Mathlib, the community library of formalized mathematics, were built into every sandbox image. The authors write that they “offered no other guidance on how to prove the theorem or organize themselves.”

The only structure imposed was a hierarchy. The lead was told to split the problem and assign parts to helpers. Helpers were told to expect work from the lead and to ask the lead when a task was unclear. During the run, the harness sent the lead 19 automatic reminders of the time remaining, each encouraging it to keep going.

Two quantities in this kit are not described. The post does not say how large the 47 lemmas are, in lines of Lean or in mathematical weight, or which parts of the proof they cover. It also does not say how detailed the 60 statements are, beyond the one-line descriptions. Both bear directly on how much of the September result the November team was given rather than rebuilt.

The harness: general tools in place of Prove2Me

September’s proof relied on Prove2Me, a platform built by Peng and collaborators at Columbia University. Anthropic’s September post says early attempts without it failed because agents “quickly lost track of the project’s state and stopped collaborating effectively.” It also says those failed efforts still contributed about 7% of the non-boilerplate lines in the final proof. The platform kept a directed acyclic graph of theorem statements so agents could see which unproved pieces were ready. It stored each statement and proof in separate files, and it provided natural-language search for reuse. Columbia’s DAPLab announcement gives the same account of why the shared dependency graph mattered.

For November, Anthropic replaced that platform with four general tools per agent:

• A shell and a file editor in a sandbox with no network access.
• Lean’s toolchain and Mathlib.
• Its own Git branch, with the ability to open merge requests into main.
• A shared Postgres database, reached from the shell.

Scale forced one design choice. The post reports that a single shared machine “hit its limits at about 100 agents.” More than half of Anthropic’s 100-agent runs had to be stopped or restarted because memory, disk or CPU ran out. So each of the 1,000 agents got its own lightweight virtual machine, connected to the outside only by a pipe to a gateway. The gateway called the Claude API and relayed Git and SQL requests to the shared repository and database.

Isolation created a new problem: 1,000 separate machines need somewhere to share state. Anthropic gave them a SQL database and gives three reasons. SQL offers general primitives for organizing information. Its transactions handle concurrent writes from 1,000 agents. And Claude is already familiar with it. The difference from September is that the lead had to design the structure itself. Prove2Me arrived with a dependency graph. Here, Anthropic says it let the lead decide how to coordinate the team, and the first thing the lead did was create tables.

Five tables in ten minutes

In its first 10 minutes, the lead created five tables:

This schema rebuilds, from scratch, part of what Prove2Me supplied. Subtasks and Landed together act as a work queue with a completion log. Notes does the job of a shared status page. What the schema lacks, at least at first, is an explicit dependency graph. That gap becomes visible later, when the team hits the hardest statement.

The database ran under fixed limits. Every call used a shared unprivileged role. Each SQL statement had a five-second time limit, and writes above 256 MiB were refused. Limits like these keep one runaway query or one oversized write from stalling the other 999 agents. They also limit what a misbehaving agent could do to shared state, though the post does not say whether agents could overwrite or delete one another’s rows.

A reconstructed timeline of the run

The post gives timestamps throughout, but they are spread across prose and figure captions. The table below puts them in order. Times are hours or minutes from the start of the run as Anthropic reports them. Where the post gives an approximate time (“about”, “around”), the table keeps that wording.

The numbers in the early entries are consistent with each other. Spreading 999 helpers over 60 statements gives 16.65 per statement, which matches crews of 16 to 17. Setting aside 47 of 60 statements after three were proved leaves exactly 10 open. Spreading nearly all 999 helpers over those 10 gives an average of about 100, inside the reported range of 46 to 139.

The timeline also shows how the lead’s role changed. In the first hour, it acted as a central planner that dealt out the statements. By hour 3, it was telling helpers to find their own work. Helpers did most of the writing to Subtasks. Anthropic quotes one helper’s note: “FREE … I finish pieces end-to-end … Name ONE deep piece … and I start at once.” The lead returned to top-down control once more, near hour 18, to send most of the team at the last large statement.

How the team handled Langlands–Tunnell

Langlands–Tunnell is a classical result that Wiles’s proof relies on. In this run, it was by far the largest single piece of work. Early on, its captain estimated that a proof would need at least 0.7 to 1 million lines of Lean and gave it less than a 1% chance of finishing in time. The lead set it aside.

When the lead returned the team to it around hour 18, many of the first tasks in Subtasks proved too large for one helper. The captain divided the statement into 10 areas and listed each piece as a task. Any helper that found a piece too big could split it and add smaller tasks beneath it. Each piece could assume the pieces beneath it, so hundreds of helpers could work in parallel before those lower pieces were proved. The tree reached 2,418 tasks up to 10 levels deep.

Anthropic reports that Langlands–Tunnell took about nine times as many tasks as any other statement and more than twice the new code. Langlands–Tunnell was proved at hour 28.4, and the final theorem followed at hour 28.7.

The task tree rebuilds, under pressure, the dependency graph that Prove2Me provided by design. It also had a weakness: the links in the tree were not recorded structurally. Anthropic notes that it “inferred most of these links afterward from the helpers’ task labels.” Without a graph enforced by the schema, the shape of the tree existed mainly in naming conventions. That evidently sufficed for the agents working in parallel, but it makes the after-the-fact audit harder.

The final statement count needs care. Anthropic’s figure tracking every helper’s work ends at 54 of 60 statements, “because five alternatives were no longer needed and one statement was dropped.” The post does not identify the dropped statement or explain why it was dropped. The reliable guard against a final proof quietly resting on an unfinished piece is to inspect the axioms the final theorem depends on. The September repository does that explicitly: its final build fails unless the theorem depends on exactly Lean’s three standard axioms. The November post does not describe its final check in that detail.

The three safety layers

Anthropic’s post presents safety as a precondition for running the experiment at all. It points back to the company’s 31 August security update. That update followed incidents in which Claude models running without cyber safeguards for evaluation reached real systems. It says the company had been “largely relying on a single layer of defense” where it needed several. The November post repeats the lesson: “no single layer of defense is sufficient to contain a team of agents.” The Frontier Wire’s account of the AISI incident and evaluation boundaries covers that background.

The identity tagging deserves attention. The gateway stamps each request with the agent’s identity outside the sandbox, which the post says prevents one agent from posing as another. In a system where the lead’s orders flow through a shared table, that matters. The post does not say how identity is recorded in the database rows themselves, since every call ran under one shared role.

Two monitors, one used

The real-time layer has a history the post sets out carefully. Anthropic ran multi-agent side-task and sabotage evaluations in which red-team agents used strategies such as decomposition attacks to try to trick the classifier into permitting a sandbox escape. Monitors that could read the agents’ chain of thought and their messages to each other caught every sabotage attempt in those evaluations. Anthropic also runs an action-only version of the same monitor, which sees what agents do but not their reasoning. It does this to guard against an agent’s reasoning persuading the monitor to permit a harmful action.

In this run, only the action-based monitor was used. Anthropic added the parallel chain-of-thought monitor “shortly after this run.” So the run went ahead with the monitor variant that was not the one reported to catch every red-team attempt. The post does not report how the action-only variant scored on those sabotage evaluations.

Anthropic also explains why it monitors this way at all. It runs experiments like this on models “that may not have completed our pre-release alignment assessment,” so it designs monitoring “for the possibility that a model is misaligned.” Released models complete that assessment first, which, in the post’s words, “reduces this risk but doesn’t eliminate it.”

What a block would have done

The post’s general description says a block stops the whole agent team until a person reviews it, so that another agent cannot carry out the blocked action. For this run it gives a narrower rule: “Only a block on the lead would have ended the run; a block on a helper removed just that helper.” The two statements describe a general policy and this run’s configuration. Under the run’s rule, a helper that triggered a block would have been removed while the lead and the other 998 helpers continued.

What “none blocked” establishes

Anthropic reports that across more than a million tool calls, none in this run met the bar to be blocked. When the calls were replayed against the chain-of-thought monitor and “today’s rubric,” only one came close: a check for root access.

This is useful evidence that the team did not take an obviously dangerous action, as judged by Anthropic’s classifier. It is weaker evidence about whether the classifier would have caught a subtle one. A zero count can mean that nothing alarming happened. It can also mean the threshold was high, or that a harmful action looked ordinary. The post does not report the classifier’s measured false-negative rate on realistic attacks at this volume, and it does not state the score threshold that defines “the bar.” The root-access check that “came close” was a probe of privilege, the kind of action the least-privilege and kernel controls exist to contain. The post does not say whether it succeeded or what the agent was trying to do.

The offline monitor’s results are not reported at all. Because it can look across agents, it is the layer best placed to notice the decomposition pattern, where an attack is split into innocent-looking steps spread over several agents. Its silence in the post is an absence of reporting, not a reported absence of findings.

The Frontier Wire’s survey of what AI review and formal checks can establish maps which question each kind of check actually answers. The same discipline applies here: a zero count from one classifier is a statement about that classifier as much as about the run.

The two formalizations compared

The headline comparison sets the November run beside September’s. The table keeps each figure with the document that reports it. It also adds the Opus 5.5 baseline, which appears only on the launch page.

Three cautions apply to this table. First, the two efforts did not solve the same problem. September’s agents worked out the structure of the proof inside Prove2Me. November’s received 60 statements that describe that structure, along with proved lemmas from the earlier work. The comparison isolates the harness and the model only partly.

Second, “one-seventh the length” needs its unit. The September post reports length in lines of Lean, and footnote 3 of that post says its proof “is likely much longer than it needs to be.” It also says failed early efforts contributed about 7% of the non-boilerplate lines. A shorter November proof could reflect better mathematics, less wasted code, reuse of the 47 supplied lemmas, or some mix of the three. The post does not separate them.

Third, the Opus 5.5 line is a single run per model, as the launch chart’s caption says. The chart’s y-axis is a “weighted share of statements proved,” and the weighting is not defined. Its data labels read 0.86 and 1.00 for Fable 5.2 and 0.26 and 0.27 for Opus 5.5, which appear to mark the 18-hour restart and the end of the run. One run cannot separate a model difference from run-to-run variance in a long, branching process. It shows the setup worked for one model on one attempt and stalled for another.

The 11 November correction

The launch page is shorter than the engineering post, and its first version described the inputs differently. An Internet Archive capture from 18:57 UTC on 9 November shows the original sentence. It said Fable 5.2 “started from minimal prompts, built its own ways to coordinate, and used no mathematical references, only a list of intermediate theorem statements to score progress.”

The current page, edited on 11 November, says instead that Fable 5.2 “started from minimal prompts, and built its own ways to coordinate.” A new footnote quotes the engineering post’s description of the starting kit, including the 47 proved lemmas from the earlier formalization. The edit note says the change was made “to more accurately describe the information we provided to the model.”

The correction matters because “no mathematical references” and “47 proved lemmas from our earlier formalization” are different claims. The engineering post, archived the same day, already had the second version. The launch page now agrees with it. Anyone who quoted the launch page on 9 or 10 November quoted the version Anthropic has since corrected. The launch page also rounds 28.7 hours to “30 hours,” which appears to match the total time available after the restart (18 plus 12) more than the time at which the final theorem was proved.

Arithmetic the posts invite

Several derived figures follow from Anthropic’s numbers. They are this publication’s arithmetic, not reported results, and each depends on the inputs shown.

Output tokens. Taking “roughly 6 billion” for September and “one-third as many” for November gives roughly 2 billion output tokens for the November run. Input tokens are not reported for either effort. For agents that repeatedly re-read long context, input tokens can be a large share of the bill.

A hypothetical price. The launch page lists Fable 5.2 at $40 per million output tokens. If 2 billion output tokens were billed at that list price, output alone would cost about $80,000. This is a hypothetical with explicit inputs. Anthropic ran an internal early version and did not pay list price. Input tokens, compute for 1,000 VMs and Lean builds are all excluded. The Frontier Wire’s editorial on coding-agent productivity argues that those excluded costs belong in any honest denominator.

Tool-call rate. “More than a million” tool calls across about 1,000 agents means at least about 1,000 calls per agent on average. Over roughly 28.7 hours that is at least about 35 calls per agent per hour, or one every two minutes or so. That rate is consistent with a loop of edit, build, check and post, in which Lean builds take much of the time. Figure 6’s caption notes that helpers were tracked “including while it waited for a build.”

Proof length. If “one-seventh the length” refers to lines of Lean, the November proof would be roughly 1.9 million lines. Langlands–Tunnell’s captain had estimated at least 0.7 to 1 million lines for that statement alone. The post gives no line count, so neither figure can be checked.

What remains unknown

The account is detailed about coordination and thin on verification. These are the open questions, roughly in order of how much they would change the reading.

The final check. The lead’s message says the theorem is “kernel-checked by the official checker.” The post does not say which checker, whether the theorem statement was compared with Mathlib’s statement of Fermat’s Last Theorem, or which axioms the proof depends on. September’s repository answers all three. It pins the axiom list to Lean’s three standard axioms, runs the leanprover/comparator tool against a challenge file, and re-checks the environment with nanoda, an independent kernel. The Frontier Wire’s guide to the artifacts behind AI-written proofs explains why statement identity matters as much as kernel acceptance.

Statement integrity. Helpers could push to their own branches and open merge requests. A separate job merged changes into main, refusing them “only in cases of a conflict or a fault.” The post does not say whether the 60 statement files were protected from edits. Proving a weakened statement would pass a kernel check while proving something else. A comparator-style check would catch it.

The dropped statement. One of the 60 statements was dropped and five alternatives were “no longer needed.” Which ones, and why, is not stated.

The size of the head start. The 47 lemmas are unquantified, as is the content of the one-sentence sketch. The released model’s training data is not discussed in the post. In particular, the post does not say whether the September repository, public since early September, could have been in the early Fable 5.2 build’s training data. Without that information, it is hard to know how much of the result is independent reconstruction.

The restart. The post says activity stopped near hour 18 and the run was restarted from its last save with 12 more hours. It does not say why activity stopped or what state was saved. The restart was Anthropic’s decision (“we restarted the run”). It also does not say whether 28.7 hours counts the gap. The launch chart shows both models resuming at 18 hours, which suggests a planned budget boundary. Still, people restarting the run and adding time is human intervention, even if it is not steering.

The monitors’ performance. There is no measured detection rate for the action-only monitor, no blocking threshold and no offline-monitor findings.

Variance. There is one run per model, and no repeated trials with different seeds.

Evidence that would change the conclusion

The following checks are proposed by The Frontier Wire. Anthropic has not announced them.

1. Release the November proof with the same verification bundle as September: a pinned toolchain, the axiom list, a comparator verdict against a Mathlib-only challenge file and an independent-kernel check. A passing bundle would turn the central claim from author-reported to independently checkable.
2. Publish the starting kit, including the 60 statements, the sketch and the 47 lemmas with their line counts. Readers could then measure how much of the proof the team actually wrote.
3. Run an ablation: the same harness with and without the 47 lemmas, and with and without the time reminders. If the run fails without the lemmas, the result is about finishing a proof, not starting one.
4. Repeat the runs, several per model, so the Fable 5.2 and Opus 5.5 gap can be compared with run-to-run spread.
5. Report the safety layers in numbers: the action monitor’s catch rate on the red-team sabotage suite, the blocking threshold and the offline monitor’s findings for this run.
6. Release the database log. The five tables, with timestamps, would let others verify the timeline above and study how the lead and helpers actually divided work.

Any one of these could strengthen the result considerably. A failed verification bundle, or an ablation showing heavy dependence on the supplied lemmas, would narrow it.

What the run does show

The clearest finding is about coordination, not mathematics. Given an empty database and no schema, a lead agent designed a workable task system in 10 minutes. It also dropped the team’s early pessimism within about an hour, after seeing its throughput. When a statement proved too large, the helpers grew a ten-level task tree by themselves. September’s early attempts without Prove2Me failed because agents lost track of the project’s state. In this run, by Anthropic’s account, the tables the lead invented kept that state for 1,000 agents.

The authors draw their own limits. They write that the result “doesn’t obviate the need for domain-specific harnesses.” They say Prove2Me may still help agents compile Lean faster and reuse human results. They also note that helpers judged 47 of 60 statements infeasible within budget, and the team went on to prove most of them. In their words, “agents tend to give up on hard problems and misjudge their difficulty,” and human encouragement can help. The run already contained a mechanical form of it: 19 automatic reminders, each encouraging the lead to keep going.

The safety account is the most transferable part for anyone running large agent teams. It shows a layered design in which no single control carries the whole burden. Identity is stamped outside the sandbox. The kernel is built without the features that would give a root user a direct path into it. Shared state sits behind an unprivileged role with hard limits. It also shows the honest limits of that design in this run: an action-only monitor, a zero-block count with no stated threshold, and an offline monitor whose results are not given.

On the evidence available on 12 November, the accurate summary is this. Anthropic reports that 1,000 agents with general tools reproduced its own Lean proof in 28.7 hours of run time. They started from a substantial head start, were restarted once and worked inside a sealed, monitored environment. The coordination findings are well described. The mathematical result will be as strong as its verification bundle, and that bundle has not yet been published.