Anthropic published research this week showing Claude produced the first complete, end-to-end, computer-checked proof of Fermat’s Last Theorem in the Lean theorem-proving language — 13 million lines of formal proof, over 5x the size of Mathlib (the community’s entire existing library of formalized mathematics), completed in 11 days largely autonomously. I want to skip past the “AI does advanced math” headline, because the number that actually matters to me as a Tech Lead is buried further down: the first attempt failed, and it only succeeded after a different team’s open-source orchestration tool, Prove2Me, got bolted on mid-run.

That’s not a story about model capability. It’s a story about long-horizon agent coordination, and it’s the most concrete public case study I’ve seen of what actually breaks when you scale an agent workload past what a single context window or a single agent session can hold.

Why Fermat’s Last Theorem is a brutal agent benchmark

Formalizing a proof this size in Lean means every one of those 13 million lines has to type-check against a proof assistant with zero tolerance for hand-waving — there’s no partial credit, no “close enough,” no informal reasoning gap the way a human mathematician might leave a step as “clearly true.” Claude’s proof establishes over 29,000 supporting theorems along the way, spanning areas of math that had never been formalized before. This means the work couldn’t be done by one agent holding the whole problem in context. It had to be decomposed, distributed, tracked, and reassembled correctly across what Anthropic describes as a team of agents running for roughly two weeks, consuming about six billion output tokens.

That’s the part worth studying regardless of whether you care about number theory.

What Prove2Me actually solved

Prove2Me, built out of Columbia University and open-sourced, maintains a directed acyclic graph (DAG) of theorem statements and coordinates multiple Claude agents against it. Two design choices stand out from an engineering perspective:

1. Separating statements from proofs into different files, linked independently. Lean compilation is slow, and re-verifying a giant monolithic proof file on every change doesn’t scale. By splitting the claim of a theorem from its proof, Prove2Me lets other agents build on top of a theorem statement before its proof is even finished — analogous to coding against an interface before the implementation lands.
2. A natural-language description attached to every theorem node, enabling search and reuse. Agents working on a sub-proof could discover that a related lemma already existed elsewhere in the DAG instead of re-deriving it — the formal-math equivalent of “don’t reinvent a utility function, search the codebase first.”

If you swap “theorem” for “microservice” and “Lean type-checker” for “CI pipeline,” this is a dependency graph and interface-first development pattern that should look extremely familiar. The novelty isn’t the pattern — it’s that a research team had to reinvent it from scratch, mid-project, because the default mode (agents dumping proof attempts into a shared context) hit a wall.

The failure mode that should worry you

The detail Anthropic reports plainly: the first formalization attempt failed. Not “produced a slightly wrong proof” — failed to complete, in a domain where “mostly correct” formal proofs are worthless because Lean rejects anything that doesn’t fully type-check. That’s a useful data point against the current narrative that scaling agent swarms mostly needs more compute and a bigger context window. It needed better coordination infrastructure — task decomposition, dependency tracking, and reuse — layered on top of frontier model capability, not instead of it.

I’d map this directly onto internal agent platforms I’ve seen (and built): the first time you try to run 20 agents against a large refactor or a big migration without a shared, queryable model of what’s already done and what depends on what, you get duplicated work, silently incompatible partial changes, and no clean way to resume after a failure. A DAG of “claims + proofs” for a math project is functionally the same infrastructure you need for a DAG of “interfaces + implementations” in a code migration.

A pattern you can actually borrow

The statement/proof separation generalizes cleanly to software agent orchestration. Here’s the shape of it applied to, say, a large-scale type migration or API refactor:

# Simplified DAG node — the "claim" (interface/contract) is tracked
# separately from the "proof" (implementation), so agents can build
# against a contract before the implementation is done.

class MigrationNode:
    def __init__(self, name, contract, depends_on=None):
        self.name = name
        self.contract = contract          # the "statement" — signature, invariants
        self.implementation = None        # the "proof" — filled in once complete
        self.depends_on = depends_on or []
        self.description = None           # natural-language summary for agent search

    def is_buildable(self, completed_nodes):
        return all(dep in completed_nodes for dep in self.depends_on)

def find_reusable(dag, query_description, embedding_search):
    # Before an agent starts new work, search existing nodes'
    # descriptions for something that already solves this subproblem.
    return embedding_search(query_description, [n.description for n in dag.nodes])

The mechanism that made Prove2Me work isn’t exotic — it’s dependency-aware task graphs plus semantic search over prior work, which most platform teams already have pieces of (build graphs, code search). The insight is that agent orchestration for genuinely long-horizon tasks needs those wired together explicitly, rather than assuming a bigger context window or a smarter model closes the gap on its own.

What I’m taking into my own agent platform work

Three things from this I’d actually apply:

• Decompose before you parallelize. Twenty agents against an undifferentiated task queue will collide. Twenty agents against a DAG with explicit dependencies and claimed-but-unfinished contracts won’t.
• Make partial work discoverable, not just complete work. The “statement without proof” pattern — publishing an interface before the implementation lands — lets downstream agents unblock immediately instead of stalling or duplicating.
• Expect the first architecture to fail on truly long-horizon work, and budget for a mid-run redesign. Anthropic’s own proof attempt needed external tooling bolted on mid-project. If a lab with this much orchestration experience hit that wall, plan your own long-running agent workloads assuming you’ll need to swap coordination infrastructure at least once before it’s stable — don’t treat your first orchestration design as final.

The theorem is the headline. The DAG-of-claims-and-proofs coordination pattern underneath it is the part I’ll still be thinking about next quarter.