Download SKILL.md: use a checked work graph with coding agents
The dependency graph behind the FLT formalization. Source: Anthropic, “Formalizing Fermat’s Last Theorem”.
Anthropic reports that dozens of Claude agents formalized an existing proof of Fermat’s Last Theorem in 11 days. They produced 13 million lines of Lean and proved 30,300 theorems, of which 29,500 were used in the final proof. The work ran through Prove2Me, a collaborative formalization platform built by Tianyi Peng and collaborators at Columbia University.
A shared dependency graph kept the 11-day project legible. Prove2Me stored theorem statements, proof submissions, dependencies, and discussions as persistent records. Each agent could query what remained open, what other agents had tried, and what would unblock downstream work. The graph held the authoritative project state; discussions supplied context around individual theorems and submissions.
I am calling the general design a checked work graph: break a large job into dependency-linked tasks with explicit contracts, then accept each result only when independent checks show it is safe for downstream work to build on. “Checked Work Graph” is a descriptive name I am proposing here, not established terminology and not Prove2Me’s own name for its architecture. The pattern has four parts. A node carries a versioned contract specifying what it must produce and what it depends on. A dependency edge records which other node’s contract or artifact this node requires. A submission is a candidate artifact for a node, tagged with the exact dependency versions it used. A check provides evidence that the submission satisfies its contract at some stated level.
The same structure works for software migrations, compiler work, data pipelines, reproducible research, and formal proof development. The checks differ in strength, but the coordination problem is the same.
Accepting partial results
Prove2Me separates a theorem’s statement from its proofs. The agent documentation describes the statement as immutable: multiple agents can submit different proofs for it without changing what other agents are trying to use.
When an agent submits a proof via POST /api/v1/verify, the server returns a status. The documented options are PENDING, ACCEPTED, SKETCH_ACCEPTED, CE (compile error), WA (wrong answer), SORRY, FAILED, or ERROR.
One mechanism that supports concurrent work is SKETCH_ACCEPTED. It means the proof verified successfully against the target type, but it imports one or more Open platform theorems. The system records the reduction. The imported theorems become the parent’s decomposition children. Someone can establish how to use a lemma while another agent works on proving it. A submission gets ACCEPTED when it checks and all its imports are already proved.
The server enforces a strict ban on sorry in agent submissions. Imported open statements have sorry bodies on the server, and those obligations remain tracked. Accepting the reduction does not mean the platform has proved its assumptions.
An agent can request GET /api/v1/theorems/:id/open-leaves to find unresolved leaves beneath a target theorem. The mission documentation says these are ranked by closability: how many ancestor theorems would automatically resolve if that leaf were proved. A leaf with closability 3 is the last missing dependency for a chain that would close three ancestors. A score of 0 does not make a theorem unnecessary; solving it just would not immediately finish anything above it. Closability measures immediate unblocking value. It does not account for task duration, so it should inform priority without controlling it.
Agents also have persistent discussions, with tags such as strategy, attempt, and reference, linked to theorem and submission IDs. The graph records what is established. The discussions record reasoning and failed approaches that the next worker may need. Anthropic describes the earlier attempts:
while agents had some early success, they quickly lost track of the project’s state and stopped collaborating effectively.
A new agent should not need to reconstruct a project from another agent’s conversation history. Here it can query the remaining work and read the notes attached to that work. The article also says failed attempts contributed about 7% of the final proof’s non-boilerplate lines.
The public agent docs describe the current protocol. They do not establish that every documented feature was used in the FLT campaign, and they do not expose Anthropic’s exact scheduler.
A higher-level map of the Mazur, Ribet, and Wiles branches converging on Fermat’s Last Theorem. Source: Anthropic, “Formalizing Fermat’s Last Theorem”.
The released FLT repository connects the finished pieces through Lean imports. Theorems/Thm_fermat_last_theorem.lean delegates to a separate solution file, which imports the supporting theorem and applies FLT.fermatLastTheorem. The final result depends on actual proofs replacing every outstanding obligation.
A software migration
The same structure applies to engineering projects where the checks are narrower. Consider migrating a codebase to a new versioned API. The graph might start as a root node for the complete migration, a child node defining the new client contract, a child for implementing that client, several children for migrating individual services against the contract, and a child for system integration and rollout checks.
The service migrations do not need to wait for the finished client. Workers can code against contract v2 and test with a fixture or mock that matches the contract. Their submissions record which contract version they used, which tests passed, and that they tested against a mock. Those results are conditional: the fixture is not the real client, so the evidence does not establish production compatibility.
When the real client artifact lands at a recorded revision, the service nodes become ready for verification. Their integration checks run against the actual client, and the coordinator records the artifact revision, dependency versions, test commands, and results. If the contract changes and becomes v3, the coordinator creates a new contract version and marks submissions built against v2 as stale or pins them to v2 until they are migrated and rechecked. The root migration becomes verified only after the required services pass their integration suite, deployment checks, and rollback checks together.
Tests provide weaker evidence than Lean proofs. A passing test suite under recorded conditions does not establish that every edge case is handled the way a formal proof would need to account for it. Builds, type checks, compatibility tests, benchmarks, production canaries, and human review all provide narrower evidence than a proof checker. Parent nodes usually become ready for verification when children complete. They do not automatically become correct. The coordinator runs the parent’s integration checks before moving it from ready-for-verification to verified.
There is overhead in maintaining this record. The pattern pays off for a migration with shared blockers, repeated handoffs, and many workers who need to recover state after losing context. It does not pay off for a small change one person can finish in an afternoon. Exploratory work where contracts cannot yet be stated should use a different structure: a log of questions, experiments, and decisions. A graph with fixed contracts imposed too early can constrain discovery.
I have not independently rebuilt the Lean proof. The mathematical claims here rely on Anthropic’s report, the public repository, and Kevin Buzzard’s review quoted in the article. Anthropic employs some of the researchers and benefits from showcasing Claude. Anthropic reports about six billion output tokens for the FLT work, which shows the project could be completed at that scale but does not give a cost comparison for a typical engineering migration.
The downloadable SKILL.md adapts this pattern for coding agents. It defines separate states for submitted, conditional, ready-for-verification, verified, and stale work. It records verification levels, revision handling, and the distinction between a mock and a completed dependency.