One Graph Beats a Swarm of Agents

Fermat's Last Theorem has been proven since 1995, when Andrew Wiles published a 129-page argument. What did not exist until recently was a machine-checkable version: the whole proof rewritten so a computer verifies every step, with no room left for "the referee missed a gap."

Anthropic says a swarm of Claude agents has now produced one. Eleven days of work, 13 million lines of Lean code, about 29,500 intermediate theorems. The mathematical community had expected that formalization effort to take years. Kevin Buzzard, who runs a competing formalization project at Imperial College London, reviewed the result, compiled the code himself, and called it a major step toward automating the formalization of the modern mathematical literature — while noting it contains no new mathematics and follows the early literature on the proof.

Those are the headline numbers. The part that should interest anyone building agent pipelines is buried lower in the story: the first attempts failed, and they failed in a way that will look familiar to anyone who has tried to run several AI agents on one project.

The swarm lost the plot before it lost the proof

The first agent teams scored partial wins, then degraded. According to Anthropic's own account, they quickly lost track of the project state and stopped working together effectively. Every agent was productive in isolation; the collective made no progress, because nobody — no thing — held the current picture of what was proven, what was being attempted, and what was already done by someone else.

If you have ever pointed three agents at the same creative brief and received three slightly different, mutually incompatible outputs, you have seen the small-scale version of this. Each agent works from its own snapshot of the task. Context drifts. Work gets duplicated or, worse, one agent overwrites the state another was building on. Adding more agents makes it worse, not better, because the coordination cost grows faster than the workforce.

The fix was a graph, not a smarter model

The breakthrough came when the team moved the work onto Prove2Me, an open formalization platform that Tianyi Peng and colleagues built at Columbia University. Its central feature is exactly one thing: a directed acyclic graph of theorem statements. Each node is a claim. Edges say which claims depend on which. Agents look at the graph and decide what to attack next; finished nodes accumulate as shared, verified state.

Two things about that design did the work. First, the graph is external to the agents. It survives their context limits and their individual failures — the article notes it counters memory degradation, meaning agents do not need to hold the whole project in their heads to avoid stepping on each other. Second, the work units are small and independently checkable. A theorem node is done only when Lean accepts the proof with nothing swept under sorry — Lean will happily compile a proof with holes, because sorry is legal syntax that quietly imports an "anything is true" axiom. Acceptance alone is not completion. Anthropic's run was additionally checked to depend on nothing beyond Lean's three standard axioms. There is no "mostly done."

That is the whole trick, and none of it is a model improvement. The same Claude agents that collapsed without it completed the project with it.

Creative pipelines have the same shape

A storyboard revision is not a theorem, but the structure rhymes. Consider a common pipeline: one set of agents generating character variants, another producing backgrounds, a third compositing shots, a fourth keeping the style guide. The failure mode of that pipeline is rarely that the models are too weak. It is that each step holds a private opinion of what the current character looks like, and those opinions diverge a little more with every pass.

The formalization world's answer transfers directly. Make the pipeline state explicit and shared: a graph where each node is an artifact with its dependencies, and a node is only "done" when something checks it. For proofs, the checker is Lean. For images, the checker is your eye plus the reference assets the shot must match. The character sheet is a node the background passes depend on; it does not update silently while three agents render against the old version.

This is also, quietly, the argument for template-first generation over one giant free-form prompt. A template is a small dependency graph you can see. "Face reference in, style block in, scene prompt in, render out" is a DAG whether or not anyone draws it. When a run fails, you know which node to re-run instead of re-rolling the entire brief.

Verified beats confident

There is a second lesson sitting next to the first. The reason mathematicians care about Lean formalization at all is that it cuts the dependence on human reviewers missing a gap. A referee can be charmed by an argument that reads beautifully; the checker cannot. What remains is a much smaller trust surface: the theorem statement says what you meant, the formalization translates it faithfully, the kernel is sound, and the imported axioms are the ones you signed off on. Anthropic's result stands or falls on whether the code compiles under those conditions — and Buzzard compiled it, which is exactly why his endorsement means something.

Agent output deserves the same suspicion. A long, fluent result from an agent is not evidence of a correct result. In the formalization runs, agents produced plenty of output that did not compile before the pipeline filtered it out. The value came from the checker, not from the volume. In creative work, the analog is refusing to let "it looks finished" stand in for "it matches the brief": pin the reference, compare against it, and treat the comparison as the completion condition.

One detail from the story keeps the whole thing honest: the big run consumed roughly six billion output tokens, which back-of-envelope math puts in the $100k–$300k range. The same platform, three private Claude Max subscriptions, and three days later a much smaller team had formalized a different theorem (Vinogradov's three primes theorem). Scale is not free, and the tooling around the model determined whether the spend bought progress or noise.

The takeaway for anyone orchestrating agents is unglamorous: the model is increasingly the part you rent, and the shared state — the graph of what depends on what, and the checker that says when a node is actually done — is the part you own. Anthropic's swarm did not get smarter mid-project. It got a whiteboard.