Claude's Agents Failed at Fermat First. The Fix Was a Task Graph, Not a Better Model.
发布于 2026-09-07
Claude's Agents Failed at Fermat First. The Fix Was a Task Graph, Not a Better Model. The headline from Anthropic's September 4 announcement is easy to write: an AI wrote the first complete computer-c...
Claude's Agents Failed at Fermat First. The Fix Was a Task Graph, Not a Better Model.
The headline from Anthropic's September 4 announcement is easy to write: an AI wrote the first complete computer-checked proof of Fermat's Last Theorem, in eleven days, largely on its own. Thirteen million lines of Lean — over five times the size of Mathlib, the community library the proof builds on.1
The more useful sentence appears further down the same post, and it is an admission of failure:
A number of Claude's initial attempts failed: while agents had some early success, they quickly lost track of the project's state and stopped collaborating effectively.2
If you are building anything with multiple agents on a long horizon, that sentence is the one worth your attention. Anthropic does not report swapping in a stronger model between the failed attempts and the successful run — what it reports changing is the coordination platform.23 So my reading is that the decisive variable was where the project's state lived, not how capable the agents were.
The failure mode is the one you already have
The pattern Anthropic describes — early progress, then a slow collapse of coordination — is the default outcome of long-horizon multi-agent work, not an exotic edge case. Agents start well because the first tasks are legible from the initial context. Then the shared picture drifts. Two agents prove the same lemma. One builds on something another abandoned. Nobody can say what is done.
#Anthropic#Claude#AI Agent#AI 基础设施
Claude's Fermat Proof: The Task Graph Mattered More Than the Model
Note that the failed attempts were not entirely discarded: those early efforts still contributed roughly 7% of the non-boilerplate lines in the final proof.2 Failed exploration produced reusable artifacts. It just could not produce a finished one, because there was nothing outside the agents holding the shape of the work.
Anthropic's fix was not a smarter agent. The effort succeeded after switching to Prove2Me, a collaborative formalization platform built by Tianyi Peng and collaborators at Columbia University, which does three specific things:3
Maintains a directed acyclic graph of theorem statements that agents read to decide what to attempt next. The post is explicit that this was what mitigated memory degradation and allowed multiple agents to work in parallel.
Separates theorem statements from proofs into different files, with links maintained independently — which speeds up Lean compilation and cuts resource consumption.
Keeps a natural-language description of every theorem statement, enabling search and reuse, which yielded a simpler proof path.
Read that list as an architecture rather than a math tool. It is: externalize the task graph, make verification cheap, and give the graph a semantic index so agents can find prior work instead of redoing it.
What Lean actually contributes
The reason this worked on mathematics first is that mathematics already had the missing piece: a checker that is cheap, total, and not a matter of opinion.
The finished proof was checked by Lean, uses only Lean's three standard axioms, and — this detail matters more than it looks — a comparator confirmed that the theorem statement being proved matches Mathlib's own statement of Fermat's Last Theorem.4 So the trust chain has exactly two human-auditable links: is this the right statement, and does the checker accept it. Nobody has to read thirteen million lines. Nobody could.
Compare that to how the human proof was validated. Wiles's 1995 proof ran to 129 pages and took months of painstaking verification; two months into the review, a reviewer exposed a critical gap that cost Wiles another year, eventually with Richard Taylor, to repair.5 The referee load is not a new problem either — when a 100,000 gold-mark prize (worth 1–2 million dollars today) was announced for FLT in 1908, 621 incorrect attempts arrived in the first year alone.6
That contrast is the whole argument for formalization, and Anthropic is careful about what it claims: unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what is novel here is the verification.7 This is a proof-checking result, not a new theorem.
Verifiable decomposition is the precondition
Here is why the DAG worked, and the part that generalizes least comfortably.
Claude produced computer-verifiable proofs of 30,300 theorems along the way, using 29,500 in the final proof.8 Each of those is a unit that can be claimed by one agent, attempted in isolation, and then accepted or rejected by a compiler without a human in the loop. That is what makes a task graph more than a to-do list: every node has a machine-decidable done state.
The human contribution shrank to match. Mathematical input from humans was limited to occasional high-level nudges from Peng — "Jacobian as a scheme sounds high priority," "push [the] Mazur [theorem] to be done soon."9 Not proving, not checking. Prioritizing nodes in a graph.
Compare that to a typical software project, where "is this feature done" often resolves to a code review, a product opinion, or a staging environment somebody has to look at. Where you have real tests, you have real DAG nodes. Where "done" means a human judgment, the graph degrades into coordination theater and you are back to agents losing track of state.
The measurement of the baseline is worth keeping in view. Formalizing FLT was expected to take years — the blueprint the community used to describe just the initial phase, following a multi-year effort Kevin Buzzard kicked off at Imperial College London in 2024, runs to 86 pages.10 The eleven days is not eleven days against a blank page. It is eleven days against a target that humans had already spent years specifying, decomposing, and partially building.
The scaffold, not the compute, is the transferable part
The obvious reading of this result is that it took frontier-lab resources: with Prove2Me and a Claude Code-based multi-agent harness, the run consumed roughly six billion output tokens from a general-purpose internal research model comparable to Claude Fable 5.1.11 Six billion output tokens is not a hobby budget.
But note that phrase — general-purpose internal research model. Not a bespoke theorem-proving system. And Anthropic reports a second experiment that undercuts the compute reading entirely: researchers using three personal Claude Max plans, collaborating entirely through Prove2Me, jointly formalized Vinogradov's Three Primes Theorem in three days.12
Three consumer subscriptions. Three days. A theorem that is a genuine result rather than a toy. The variable that carried across both runs was not model scale or spend — it was the coordination substrate. That is my inference rather than Anthropic's claim, but it is the inference the two data points invite: if the scaffold is what makes agent collaboration hold together, then the scaffold is the part you can copy without a frontier lab's budget.
The artifact itself is public and independently checkable. The anthropics/fermats-last-theorem repository was created on 2026-09-04, lists Lean as its primary language, occupies about 232,565 KB, and had 843 stargazers when I queried the GitHub API.13 You do not have to take the blog post's word for the existence or the language of the thing.
What this does not tell you
Three limits worth stating plainly, because the milestone framing tends to erase them.
It does not show that agents can do open mathematical research. Claude followed a simplified version of Wiles's proof from Darmon, Diamond and Taylor.14 The route existed; the work was rendering it in a form Lean accepts.
It does not show that eleven days is the true cost of the result. Add the 86-page blueprint, the community formalization effort since 2024, and the discarded first attempts that survived only as 7% of the final non-boilerplate lines,210 and the honest framing is that a large human-built scaffold was converted quickly, not that the problem was solved from scratch quickly.
And it does not transfer to domains without a Lean. If your correctness oracle is a human reviewer, you do not get to skip reading the output. The reason nobody needs to audit thirteen million lines here is that a compiler already did, against a statement that was checked to be the right one.4 Strip that out and you have thirteen million lines of unreviewed generated code — which is not a proof of anything.
The actual takeaway for builders
If you are running agents on work that spans days rather than minutes, the lesson of this project is not "use more agents" or "wait for a better model." Both of those were available in the attempts that failed.
The lesson is that long-horizon agent work needs its state stored outside the agents, in a structure that answers three questions without consulting a model: what is done, what is claimable now, and what already exists that I should reuse. Anthropic's version of that answer was a DAG of theorem statements, statements split from proofs so the compiler runs fast, and natural-language descriptions so agents could search prior work.3
Every one of those has an analogue in ordinary software: a dependency graph of tasks with machine-checkable completion, a fast test suite, and a searchable index of existing work. The FLT proof is the most spectacular demonstration so far of what those three things buy you when they actually exist — and a precise diagnosis of what breaks when they do not.