One Thousand AI Agents, One Proof: What the Lean Experiment Actually Shows

When a thousand AI agents work on one problem, the model is only part of the system. The other part is how the agents divide work, exchange state, submit changes and learn that a result is valid.

On November 9, Anthropic described an experiment in which a team of approximately 1,000 agents running an early version of Claude Fable 5.2 reproduced a formal proof of Fermat’s Last Theorem in the Lean proof assistant. The company reports that the run took 28.7 hours. This was a research experiment reported by the company, not a general benchmark for software teams.

The first distinction matters: the agents did not discover Fermat’s Last Theorem or replace Andrew Wiles’s proof. The task was to formalize an existing mathematical result so that a proof assistant could check its steps. That is substantial engineering and mathematical work, but it is a different claim from inventing a new proof.

The team had a map and tools

Anthropic’s technical account says the agents received 60 statements to prove, including 59 intermediate milestones and the theorem itself. They also received a short sketch of the classical route, relevant definitions and 47 proven lemmas from the team’s earlier formalization. Those inputs are part of the result; they were not solving the problem from a blank page.

The researchers assigned one lead agent and 999 helpers. Each agent had its own sandbox, a shell, a file editor, the Lean toolchain and Mathlib. They worked on separate Git branches, submitted changes for merging, and used a shared PostgreSQL database for task claims, notes and completed work. A grader checked submitted proofs.

The point I keep returning to is that shared state did not make the answer correct by itself. It made parallel work possible. The proof checker gave the team a separate way to evaluate the mathematical artifacts produced by that work.

Coordination and verification are different jobs

A shared database can tell agents which subproblem is available. Git can preserve changes and expose conflicts. Neither automatically proves that a mathematical claim follows from the stated assumptions. Lean checks a formal proof against its definitions and rules; the value of the result also depends on what those definitions and assumptions actually express.

This is why I would resist translating the headline directly into “a thousand agents can solve any hard problem.” The experiment had an unusually useful structure: researchers could describe milestones, previous formal work supplied lemmas, and there was a concrete checker. Many software and business tasks are less clear about what counts as a correct outcome.

The comparison in Anthropic’s announcement is also narrow. Its chart reports a single run per model in that setup. Faster formalization in one configured experiment does not establish a general speedup or reliability guarantee for other teams, tasks or budgets.

The safety boundary was engineered

Anthropic describes a separate lightweight virtual machine for each agent, no direct network access from those sandboxes, and a gateway for approved Git and database requests. A real-time classifier checked tool calls, while an offline monitor reviewed actions. The company says no action in this run met its threshold for blocking.

Those details matter because parallel agents increase the number of actions a system must observe. A monitor and a sandbox can reduce risk, but their presence is not proof that every possible failure or escape is impossible. The useful question is what the system can do, what each control can actually stop, and how a person can inspect or intervene.

What I would take into an engineering project

Before adding more agents to a project, I would make the acceptance signal explicit. What evidence shows that a task is finished? Which assumptions are outside the checker? Where does shared state live, and who can change it?

Start with work that can be divided without overlapping writes. Keep the artifacts and decisions visible. Give each worker the minimum access needed. Then measure whether coordination, verification and review still work as the number of workers grows.

The interesting part of this experiment is not simply the size of the team. It is the combination of a bounded problem, supplied mathematical context, shared coordination and an executable check. Those ingredients are much harder to summarize in a headline—and much more useful when designing an agent system.

Sources

• Anthropic: Claude Fable 5.2 and Mythos 5.2, November 9, 2026.
• Claude.dev: Safely scaling multi-agent teams with Claude Fable 5.2, November 9, 2026.
• Lean: official logo and trademark policy. The unmodified Lean logo and its trademark symbol identify the proof assistant; use does not imply endorsement by Lean FRO.

Sources reviewed November 11, 2026. Follow jpalanco.com for more notes on AI, engineering and open-source tools.