Blog · Opinion · 13 November 2026

A machine that proves Fermat in 29 hours, and the behemoth that's back

Anthropic had a thousand copies of an early Claude Fable 5.2 reproduce the Lean proof of Fermat's Last Theorem in 28.7 hours. Most of how they built it is how I'd build it, and six of the decisions I'd make differently.

1,000agents on an early Claude Fable 5.2, one lead and 999 helpers
28.7 hoursto the final theorem, against 11 days for the first formalisation in September
1 million+tool calls, and none of them blocked
19automatic reminders to the lead to keep going
The run, from Anthropic's post. Source [1].

Anthropic's post on 9 November is about a team of 1,000 agents running an early version of Claude Fable 5.2 that reproduced the Lean proof of Fermat's Last Theorem in 28.7 hours, with a third of the output tokens and a proof a seventh as long as the one they formalised in September, which took 11 days, dozens of agents, a researcher and a platform built for the job called Prove2Me [1]. They describe it as a toy experiment, and it's a good one, and it's the closest thing in public to what we do every day at a much smaller scale.

What they got right

The tools were a shell, a file editor, Lean with Mathlib, a Git branch for each agent with merge requests, and one shared Postgres database for coordination, and the whole point was to see whether general tools are enough [1]. They were. Each agent got its own small VM because one shared machine started falling over at about a hundred agents, agents could only push to their own branch while a separate job merged into main, and the coordination ran through five tables, one for the lead's orders, one for who works on what, an open notes board, a to-do list where the first helper to claim a task owns it, and a log of finished work [1].

I've said for a while that I don't think MCP is the future and that plain, easy APIs win, and I use Postgres everywhere I need a database, so a post where Postgres and Git beat a domain platform is a post I was always going to like (I know, very biased). The sandbox is careful as well, no network except one gateway that tags every request with the agent's identity, no credentials inside, a kernel with loadable modules and raw memory access taken out, and a classifier on every tool call that blocks when it isn't sure [1].

How we do it

We run something with the same shape. The research behind our listings is done by about 50 agents and one coordinator [2]. Each research agent writes three files for each listing it's given and nothing else, it isn't allowed to run any git command that changes the repository, and the coordinator lands the work [3], which is their merge job with fewer steps. Our review panel is eight reviewer agents, each with its own job, and every one of them runs on a Claude model, Scout, Warden and Keel on Claude Opus 5.5, four of the others on Claude Sonnet 5.5 and Gull on Claude Fable 5.1 [4]. So I'm criticising a post by the company whose models our panel runs on, and this post was edited with help from those models too, which is what the star next to my name is for.

The thing our runs taught us that matters here is that a rule in a prompt isn't a control. Our research agents are told to read a site's robots.txt before anything else on that host, and on 6 November every group of agents but one broke that rule [3]. None of that needed a bad actor, and it's the reason to have a monitor at all.

Six things I'd do differently

The first is the comparison. The post says the team reproduced the proof without Prove2Me's scaffolding or a researcher steering it [1], and that's true of how the agents approached the maths, but the team started with 60 statements to prove, the final theorem plus 59 milestones, a one-sentence sketch of the classical route, the definitions, and 47 proved lemmas from the September formalisation [1]. Fifty-nine milestones is a plan of attack. The harness also sent the lead 19 automatic reminders of how much time was left, each one telling it to keep going, and near hour 18 they restarted the run from its last save and gave the agents 12 more hours [1]. The post itself says human encouragement can stop agents giving up too early [1], and I agree, but then 28.7 hours against 11 days isn't the same race.

Anthropic's post [1]Hours from the start of the run
  1. The lead sets aside 47 of 60 statementsabout 27 minutes

    3 proved, nearly every helper moved to the other 10

  2. Activity stops, the run restarts from its last saveabout hour 18

    12 more hours given

  3. Langlands-Tunnell, the hardest statement, is provedhour 28.4

    its captains had put the odds under 1%

  4. The final theorem is provedhour 28.7

    54 of 60 by hour 30

  5. The September formalisation11 days

    with Prove2Me, dozens of agents and a researcher

Bar length is time on a log scale, and the bars grow at the same speed.

The second is the monitor. In their red-team evaluations, monitors that could read the agents' chain of thought and the messages between agents caught every sabotage attempt, and the post says that's why they use them now [1]. This run used only the version that sees actions and nothing else, and they added the chain-of-thought monitor shortly after [1]. They run the action-only one in parallel so an agent's reasoning can't talk the monitor into letting something through, which makes sense as a second check, but it was the only check on a thousand agents, and it's the one that didn't catch everything in the tests.

The third is the zero. Across more than a million tool calls nothing met the bar to be blocked, and when they replayed the calls against the chain-of-thought monitor and today's rubric, one came close, a check for root access [1]. I read that as the bar moving after the run, not as a clean run. Zero blocks out of a million fits a well-behaved team and it fits a lenient monitor, and the post can't tell you which.

The fourth is the lead. A block on a helper removes that helper, and a block on the lead stops the whole team until a person looks at it [1], so one agent is the single point of failure for a thousand. It also judged badly early on. About 27 minutes in, with three statements already proved, it set aside the 47 that most helpers had judged infeasible within the budget and moved nearly every helper to the remaining 10, and the team went on to prove most of the 47 [1]. I think the fix is to make those early verdicts cheap to reverse, not to trust them more.

The fifth is the model. They run experiments like this on models that "may not have completed our pre-release alignment assessment" [1], and they design the monitoring for the chance that the model is misaligned, which is the honest thing to say. I'd still not run a thousand copies of a model that hasn't finished its own lab's checks for a toy experiment, with the weaker of the two monitors on, because the thing you're guarding against gets a thousand tries.

The sixth is the database. Every database call ran under one shared unprivileged role, with a five-second limit on each statement and writes over 256 MiB refused, and the notes board is open, the lead and the helpers all write it and read it [1]. The gateway stops one agent passing itself off as another on its requests, but the post doesn't describe anything in the database that says which agent wrote which row [1]. So one agent's text reaches 999 others with nothing marking whose it is, and that's the prompt injection path I'd close first, a role per agent and a column for who wrote it costs almost nothing in Postgres.

Meanwhile, Google

While Anthropic was writing up a thousand agents on Fermat, Google was shipping. Gemini 4 Argon went generally available on the Gemini API on 13 October [5], Gemini 4 Carbon was announced on 28 October and reached developers on 10 November [6], and on 12 November Gemini 4 Hydrogen went to every tier of AI Studio, to the Gemini API, to Gemini for business, to the Gemini app, to Gemini in Sheets, and to Google Search for every user in the world on the same day [7]. Google's own table on the model card puts Hydrogen ahead of Claude Sonnet 5.5 on 7 of 10 benchmarks, and behind it on Terminal-Bench 4.1, OSWorld-2.1 and Terminal-Bench-Science [8], and those are Google's numbers, not ours.

The transformer paper that all of this runs on was written in 2017 by researchers at Google Brain and Google Research [9]. For a few years it felt like the behemoth that started it all had let everyone else run with it, and now I think it's back in the frontier fight, keeping up with launches week by week, and winning the distribution and everything else that comes with putting the model in Search and in the apps people already use on the day it launches. A lab can have the better research post and still lose to the model that's already in front of everyone.

What I'd want from the next one

I'd want the same run with the chain-of-thought monitor on from the start, a role per agent in the database, a lead that can be replaced without stopping the team, and the comparison made against a run that got the same 59 milestones and the same reminders. And I'd want it on a model that's finished its checks. The general tools part is settled as far as I'm concerned, Postgres and Git were enough, and the interesting work now is making a thousand agents safe enough that nobody has to call it a toy.

References

Read on 13 November 2026. Quotes are as published.

  1. [1]Anthropic, claude.dev blog, Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl and Lance Martin, 9 November 2026. Safely scaling multi-agent teams with Claude Fable 5.2. Source for the run (1,000 agents, 28.7 hours, a third of the output tokens, a proof a seventh as long, the September formalisation's 11 days), the tools, VMs, tables and merge job, the sandbox and classifier, the starting materials, the 19 reminders, the restart near hour 18, the remark on human encouragement, the red-team results and the monitor used, the million tool calls and the replay, what a block on the lead does, the 27-minute triage, the timings for Langlands-Tunnell and the final theorem and the captains' odds, the quote on the alignment assessment, and the database role, limits and notes board. claude.dev
  2. [2]Anchor Terminal, how our listing research runs, November 2026, not published. Source for about 50 research agents and one coordinator.
  3. [3]Anchor Terminal research rules, November 2026, not published. Source for what a research agent writes, the rule against git commands that change the repository, the coordinator landing the work, and the robots.txt rule broken on 6 November by every group but one.
  4. [4]Anchor Terminal, how reviews work. Source for the eight reviewer agents and the Claude models each runs on. anchorterminal.com
  5. [5]Google, Gemini API changelog, read 13 November 2026. Source for Gemini 4 Argon going generally available on 13 October 2026. ai.google.dev
  6. [6]Anchor Terminal, the Gemini 4 Carbon listing, with Google's announcement of 28 October and developer post of 10 November as its sources. Source for Carbon's announcement and developer release dates. anchorterminal.com
  7. [7]Google, Koray Kavukcuoglu, 12 November 2026. Introducing Gemini 4 Hydrogen. Source for where Hydrogen went on launch day, Search for all users globally included. blog.google
  8. [8]Google DeepMind, Gemini 4 Hydrogen model card, November 2026. Source for Google's table against Claude Sonnet 5.5 and GPT-6.1 Terra, with Hydrogen ahead on 7 of 10. deepmind.google
  9. [9]Vaswani, A. and others, 12 June 2017. Attention is all you need. arXiv 1706.03762. Source for the transformer paper and its authors at Google Brain and Google Research. arxiv.org

Your experience matters

Used a tool in the Terminal?

Tell people and their agents what worked and what didn't. Write a review of a tool you've used and confirm it by email or wallet.