DAG, not chat: how Claude formalized Fermat's Last Theorem in Lean

On September 4 Anthropic published that Claude had produced the first complete, end-to-end, computer-verified proof of Fermat's Last Theorem in Lean. The run happened in August on a platform called Prove2Me, built by Tianyi Peng at Columbia, and took about 11 days, mostly autonomously. The output is roughly 13 million lines of Lean, 30,300 theorems proved, of which about 29,500 are used in the final proof, at a cost of around 6 billion output tokens. Human input was limited to occasional high-level direction. Lean checked every step.

I care less about the theorem than about the method, because the method is a production pattern.

It was not one long context

This was not one model thinking for 11 days in one enormous conversation; no context window holds 13 million lines. Prove2Me runs many Claude agents against a directed acyclic graph of sub-claims. The theorem at the root decomposes into lemmas, the lemmas into smaller lemmas, and each node is a bounded task: given these hypotheses, prove this statement, in Lean, so that the checker accepts it. Agents take nodes, produce candidate proofs, and the Lean kernel accepts or rejects. Accepted nodes become available to their parents. Rejected ones go back on the queue.

Three properties make this work, and they are exactly the properties most agent deployments lack.

• Decomposition into a graph, not a list. Nodes with no shared dependencies run in parallel; nodes that depend on unfinished work wait. Throughput comes from the width of the DAG, not the size of the model.
• A verifier that is not the model. Lean does not care how confident Claude sounded. Every one of the 30,300 theorems was accepted by a kernel that cannot be persuaded.
• Bounded tasks with explicit interfaces. A node's contract is its hypotheses and its goal. Agents cannot drift, because drift fails the check.

Reliability came from coordination over a graph with a verifier at every node, not from a bigger model or a longer context.

The pattern transfers to code

Swap theorem for requirement and Lean for the test suite, the type checker and the invariant checker, and you have spec-driven development with agents. The root node is the feature. Child nodes are components with typed interfaces. Leaf nodes are functions with property tests. An agent takes a leaf, produces an implementation, and the verifier accepts or rejects.

Most agent fleets today do the opposite: one long session, a vague goal, the model as its own judge. That is a chat, and chats do not scale. A study on arXiv (2608.28147, August 2026) makes the point: across five Qwen models on eight engineering tasks in a process simulator, adding a single instruction, re-run the simulation after every substantive change, took re-verification from 32 of 120 runs to 94, and bounded success from 35 of 120 to 95. One sentence about verification cadence nearly tripled success. Fermat is the same idea with the cadence enforced by the graph instead of the prompt.

The missing piece in most parallel fleets is the verifier gate between nodes; Codex parallel fleet covers the coordination side and guardrails and output validation the checking side.

What to build this quarter

• Write the DAG before the prompt. If you cannot draw the dependency graph of the work, an agent cannot execute it reliably either.
• Make every node's acceptance mechanical. Tests, types, a schema, a proof. If a human has to read the output to know whether it is right, the node is not done.
• Budget per node, not per run. Six billion tokens is a real invoice. Per-node budgets tell you which sub-claim is burning money.
• Watch the Lean ecosystem. Mistral's Leanstral 1.5, a Lean 4 proof-engineering model, shipped in late July; formal gates are maturing on the open side too.

The honest gap

Anthropic's post gives totals, not the shape of the run: how the DAG was built, how many nodes failed and were retried, how theorems were deduplicated, and what the occasional high-level direction from humans actually consisted of. Those details decide whether the pattern reproduces on your problem or only on a theorem with a century of published structure to lean on. Lean makes the result trustworthy; it does not make the process transparent.