checked work graphs for multi-agent projects

Download SKILL.md: use a checked work graph with coding agents

Formalization of Fermat's Last Theorem shown as a large radial dependency graph. Fermat's Last Theorem sits near the center, with thousands of theorem nodes branching into labeled areas including Mazur's theorem, Ribet level lowering, Wiles modularity lifting, Neron models, Langlands-Tunnell, Taylor-Wiles primes and Selmer groups, Shimura curves, and Galois representations.

The dependency graph behind the FLT formalization. Source: Anthropic, “Formalizing Fermat’s Last Theorem”.

Anthropic published a wild writeup recently: dozens of Claude agents formalized a proof of Fermat’s Last Theorem in Lean in 11 days. 13 million lines of Lean, 30,300 proved theorems (29,500 used in the final proof). They ran the whole thing on a platform called Prove2Me built by Tianyi Peng and folks at Columbia.

The interesting engineering question here is: how do you keep dozens of agents working on a massive 11-day project without losing track of state or stepping on each other?

In their early runs without a coordination platform, Anthropic noted:

while agents had some early success, they quickly lost track of the project’s state and stopped collaborating effectively.

What fixed it was putting a shared dependency graph with strict verification in the middle. I’ve been calling this pattern a checked work graph (my name for the pattern, not Prove2Me’s):

Nodes have a versioned contract (the theorem statement or interface spec)
Edges track which nodes depend on which other nodes
Submissions are candidate implementations/proofs attached to a node
Checks verify the submission independently before marking the node done

How Prove2Me lets agents work in parallel

If you look at the Prove2Me agent docs, a theorem’s statement is immutable, so multiple agents can try proving it or using it without changing the contract underneath other agents.

When an agent submits a proof to POST /api/v1/verify, the server returns one of: PENDING, ACCEPTED, SKETCH_ACCEPTED, CE (compile error), WA (wrong answer), SORRY, FAILED, or ERROR.

SKETCH_ACCEPTED is the clever part. Suppose Theorem A depends on Lemma B, and Lemma B isn’t proved yet. An agent can still prove Theorem A assuming Lemma B holds. The server verifies that the proof of A compiles against B’s type signature (with zero sorry allowed in the agent’s own code), marks A as SKETCH_ACCEPTED, and tracks Lemma B as an open child obligation. Once another agent proves B, A flips to ACCEPTED.

That means agents don’t have to work strictly bottom-up and block on every leaf lemma before testing higher-level structure.

To decide what to work on next, agents hit GET /api/v1/theorems/:id/open-leaves. According to the mission docs, open leaves are ranked by closability - how many parent theorems immediately flip from SKETCH_ACCEPTED to ACCEPTED if you finish that leaf.

Agents also post notes to persistent discussions tagged with strategy, attempt, or reference right on the theorem ID. So when a fresh agent picks up a theorem, it doesn’t need the previous agent’s full chat transcript - it just reads the node’s discussion thread to see what already failed. (Anthropic mentioned failed attempts still contributed ~7% of the non-boilerplate lines in the final repo.)

A simplified dependency map with three colored branches labeled Mazur, Ribet, and Wiles. Their intermediate results converge through the Frey curve construction and the modularity and level-lowering results into Fermat's Last Theorem.

High-level map of the Mazur, Ribet, and Wiles branches converging on Fermat’s Last Theorem. Source: Anthropic, “Formalizing Fermat’s Last Theorem”.

In the final public repo, Theorems/Thm_fermat_last_theorem.lean pulls the proved modules together via Lean imports and applies FLT.fermatLastTheorem.

Using the same pattern for software migrations

Obviously unit tests and integration tests aren’t as watertight as the Lean typechecker, where a typechecked proof is 100% done. In normal software, a green test suite on a child task doesn’t guarantee the parent service won’t blow up in integration.

Still, the coordination structure translates really well to big multi-service migrations. Suppose you are migrating 10 services to a v2 API client:

Root node: full migration verified
Contract node: v2 API schema/types locked at revision v2.1
Client node: implement the v2 client library
Service nodes (x10): migrate each service to v2

Just like SKETCH_ACCEPTED, the 10 service agents don’t need to wait for the real v2 client to finish first. They can code against the v2.1 contract using a mock/fixture, pass their local unit tests, and mark their node conditional (the software equivalent of SKETCH_ACCEPTED).

Once the real v2 client lands, those 10 service nodes move to ready-for-verification and run real integration tests against the actual client revision. And if someone bumps the contract to v2.2, any submission pinned to v2.1 automatically gets flagged stale so you know exactly which services need to be re-run.

Is this overkill for a 2-hour feature? Yes, 100%. Don’t build a dependency graph for something one agent can do in a single session.

Where it pays off is big refactors or migrations where multiple agents (or sessions across days) keep losing track of what’s mocked vs what’s actually verified end-to-end.

I packaged this state machine (submitted, conditional, ready-for-verification, verified, stale) into a skill you can drop into Claude Code / Codex / Hermes: Download SKILL.md.