What Fermat's Last Theorem Formalization Reveals About Multi-Agent Collaboration

Anthropic's September 2026 project had Claude autonomously formalize Fermat's Last Theorem in Lean over 11 days, producing roughly 13 million lines of Lean code, 30,300 machine-checkable theorems (29,500 used in the final proof), consuming about 6 billion output tokens, with dozens of Claude agents collaborating. The goal was not new mathematics but a stress test of long-horizon multi-agent collaboration.

Why Multi-Agent Systems Lose Control

A study of five open-source multi-agent frameworks across 150+ execution traces identified 14 failure modes grouped into three categories: specification and system design issues, inter-agent inconsistencies, and task verification/termination problems. Failures often occur between agents, not within a single model response. Examples include upstream agents omitting input versions, downstream agents proceeding anyway; two agents interpreting the same field differently with no clarification mechanism; and verifiers checking only syntactic compilation, not functional correctness. Clearer role prompts and orchestration help but cannot fully replace state management, evidence tracking, and termination decisions. Short demos succeed because context stays short, versions don't proliferate, and humans judge the final result. Once tasks run for days with dozens of intermediate artifacts, chat history cannot serve as a project database.

Parallelism Requires Explicit Work Units

Prove2Me structures work as a DAG where nodes are explicit theorem statements and edges are dependencies. Target X proceeds only when its prerequisite theorems A, B, C are satisfied. This turns parallelism from "multiple agents chatting simultaneously" into multiple well-bounded, independently verifiable work items. The DAG externalizes four critical facts: current goal, required upstream results, completed nodes, and blocked nodes. Agent context may change, but the graph's facts persist beyond any single conversation.

Planning Must Follow Evidence

Complex tasks cannot be fully decomposed upfront. Anthropic researcher Tianyi Peng occasionally gave high-level hints (e.g., "prioritize Mazur's theorem"), but specific definitions, lemmas, and transformations emerged during execution. The Prove2Me graph grows with the proof: when an agent finds a direct proof of X infeasible, it proposes A, B, C as prerequisites; if A remains too hard, it further decomposes A. New nodes enter the shared graph with their own dependencies and artifacts, not confined to the proposing agent's context. As execution advances, the plan rewrites alongside the evidence. This differs from traditional one-shot planners; dynamic planning requires constraints: each new node must address a specific gap, declare explicit dependencies, and have a designated verifier. Without these, dynamic planning becomes uncontrolled todo-list growth.

Handoffs Must Leave Reusable Artifacts

Typical multi-agent handoffs pass a summary paragraph, which mixes facts, conjectures, and state. Prove2Me uses concrete handoff objects: a theorem statement and its proof file. Agent B does not trust Agent A's claim; it loads the theorem via the dependency graph and asks Lean to re-verify. Two complementary designs: separate storage of theorem statements and proofs to reduce compilation overhead, and natural-language descriptions for each statement to enable search and reuse. Together they create a shared library of sourced, dependency-tracked, verified artifacts — not a larger chat log. Andrej Karpathy's context engineering principle aligns: the next model needs the right task, tools, state, and relevant data, not more history. Prove2Me retrieves only nearby reusable results for the current goal instead of stuffing 30,000 theorems into context.

Verifiers Gate State, They Don't Plan

Lean acts as an independent verifier. Agents propose proofs or proof sketches ("if A, B, C hold then X follows"), but only Lean-checked results enter the verified shared library. Lean cannot judge whether A, B, C are the best decomposition or the most resource-efficient path. A comparator also checks that the formalized theorem statement matches Mathlib's Fermat statement, and the final proof uses only Lean's three standard axioms. Two boundaries exist: proof code passes mechanical checking, and the target proposition corresponds to the established mathematical library. Machine verification does not equal human understanding; Anthropic notes formal proofs address verifiability, not readability, conciseness, or mathematical elegance. In general agent systems, reviewers must be separate from generators, and verification results must mutate task state. A code agent submits an implementation; a test system checks behavior. A research agent proposes a conclusion; a rule engine checks constraints. A verifier that only emits opinions without authority to block faulty artifacts is a commentator, not a system component. Verification is not a panacea: unclear requirements, role overreach, and communication inefficiencies can derail tasks before final acceptance.

Conflicts Require State and Version Management

Anthropic notes the initial attempt failed to collaborate naturally: agents quickly lost project state, though failed attempts still contributed ~7% of non-template code. Model improvements don't auto-resolve conflicts. The system must assign agents to distinct nodes to minimize concurrent edits on shared objects, give tasks and artifacts stable identities so old results don't silently overwrite new ones, and record each attempt's input snapshot, output, and verification status. A recoverable work item minimally includes: goal, parents (upstream dependencies), snapshot (input version at start), artifact (code/proof/data), status (candidate, running, verified, conflict, abandoned), attempt (execution count and retries). Chat messages suit event passing, not global state. After scheduler restarts, context switches, tool timeouts, or agent replacements, the system must still answer "what step are we on?".

goal         current objective
parents      upstream results this goal depends on
snapshot     input version at task start
artifact     produced code, proof, or data
status       candidate, running, verified, conflict, abandoned
attempt      current execution number and retry count

Five Collaboration Actions from the Fermat Project

Define verifiable artifacts first, then decide how many agents. The project parallelized over theorem nodes, not roles like researcher/programmer/reviewer. In general engineering, the unit can be an interface implementation, a dataset, or a compliance rule — each with clear inputs, outputs, and acceptance criteria.

Let the plan grow with evidence, writing changes back to the task graph. Agents add prerequisite nodes when proofs stall; the scheduler adjusts downstream work. The portable experience is the recorded dependencies, rationale, and next-step ownership — not changes trapped in an agent's temporary context.

Handoff files, dependencies, and verification status — not "I'm done." Theorem statement, proof file, and natural-language description together let the next agent find, reuse, and re-verify. Code, data, and document collaboration need similar artifact boundaries.

Make verification results actually change state. Lean passes → node enters reusable library; verification fails → task returns to repair or re-plan, not just generate another explanation. Tests, rule engines, and human approvals in ordinary systems need the same rollback authority.

Give every attempt an identity and a recovery entry point. Input snapshot, attempt number, artifact address, and failure reason let the system distinguish "not started," "done but unverified," and "stale agent late write." This beats compressing everything into a long summary.

Anthropic's multi-agent coordination patterns article classifies five structures: Generator-Verifier, Orchestrator-Subagent, Agent Teams, Message Bus, and Shared-State, advising to start with the simplest pattern that meets the need and upgrade only when a concrete bottleneck appears. The Fermat project combines several: Agent Teams for parallel exploration, Shared-State for the theorem graph and artifacts, Generator-Verifier with Lean gating errors, and the Claude Code shell for scheduling and recovery. Pattern selection maps to task bottlenecks:

High-quality acceptance needed → start with Generator-Verifier.

Clear sub-task boundaries, few dependencies → Orchestrator-Subagent suffices.

Independent exploration, long runtimes → Agent Teams adds parallel value.

Continuous event streams, growing participants → Message Bus fits.

Multiple agents persistently working on the same intermediate results → Shared-State justifies investment.

Anthropic's earlier Research system showed parallelism's limits: on breadth-first problems requiring many independent directions, an Opus 4 lead with Sonnet 4 subagents outperformed a single Opus 4 by 90.2%, but token consumption was ~15x normal chat. They observed simple questions spawning 50 subagents, repeated searches for non-existent sources, and invalid updates. Parallelism expands exploration capacity while amplifying coordination, cost, and termination challenges. Therefore, the decision to use multi-agent should start from whether the task decomposes into relatively independent directions with verifiable outcomes, not from "how many agents."

Returning Shared State to the Engineering Floor

Recent discussions on Agent Teams, Harness, and Skill all touch the same boundary: context helps agents judge, but task state, versions, and verification evidence cannot live only in context. The Fermat project makes this boundary visible in a continuous long task. Stripping away mathematical details, Prove2Me plus the Claude Code runtime shell maps to a familiar engineering stack:

Task Graph: records goals, dependencies, executable nodes → leaves node relationships, versions, status.

Artifact Store: stores code, proofs, data, descriptions → leaves artifact addresses, provenance, attempt numbers.

Retrieval Layer: loads most relevant context for current node → leaves query conditions and recall results.

Agent Execution Layer: generates local proposals, adds nodes, fixes failures → leaves tool calls, inputs/outputs, attempt logs.

Verifier: checks compilation, tests, rules, formal constraints → leaves verification commands, reports, conclusions.

Scheduling & Recovery Layer: handles claiming, retries, expiration, human intervention → leaves event logs, leases, recovery reasons.

In ordinary multi-agent projects, upstream cannot hand off just a conclusion; completion cannot rely on an agent's reply; failure cannot trigger a full re-run; unknown state cannot be treated as failure.

When Does a DAG Help?

DAGs suit tasks where: the goal decomposes into dependent sub-problems, sub-artifacts are independently verifiable, verification results persist, and later work can reuse confirmed results. Formal mathematics meets these criteria. Software builds, data processing, and compliance rule checking may satisfy some. But when requirements are still shifting, acceptance criteria are unformed, dependencies are highly implicit, or results require domain experts to judge contextually, drawing a pretty DAG creates false certainty — edges look clear but business meaning is unconfirmed. Cost cannot be ignored: ~6 billion output tokens for Fermat; the machine-checked proof is likely far longer than a human mathematician's version. Verifiable ≠ cheap; reusable nodes ≠ optimal path. A smaller control experiment: three personal Claude Max plans via Prove2Me formalized Vinogradov's three-prime theorem in 3 days. This doesn't compare directly to Fermat's scale, but signals that in formalization tasks, collaboration viability depends not only on model size or account count, but equally on task graph, shared artifacts, and verification loops.

Bringing the Lessons Back to General Systems

The transferable practice is establishing shared state around long tasks. Software construction, data processing, research retrieval, and compliance checking — any domain where sub-tasks, artifacts, and acceptance criteria can be clearly defined — can borrow from this; Lean and theorems are merely the vehicle. The runtime design perspective: agents propose and execute local proposals; the system persists goals, dependencies, evidence, verification results, and recovery paths. Formal mathematics fits because theorem dependencies are clear, Lean verifies independently, and artifacts are long-lived reusable. When requirements flux, acceptance criteria are absent, or expert synthesis is required, forcing a DAG creates an illusion of certainty. For short, low-dependency tasks, a single agent with a few tool calls suffices. Once tasks lengthen, stuffing summaries into context only makes the system harder to audit. Multi-agent is worthwhile only when the system prepares a shared, verifiable state for collaboration.

References

Anthropic, Formalizing Fermat's Last Theorem (https://www.anthropic.com/research/formalizing-fermats-last-theorem)

Anthropic, Multi-agent coordination patterns: Five approaches and when to use them (https://claude.com/blog/multi-agent-coordination-patterns)

Anthropic, Patterns and problems in emerging multiagent systems (https://www.anthropic.com/research/multiagent-systems)

Anthropic, Building multi-agent systems: When and how to use them (https://claude.com/blog/building-multi-agent-systems-when-and-how-to-use-them)

Mert Cemri et al., Why Do Multi-Agent LLM Systems Fail? (https://arxiv.org/abs/2503.13657)

Prove2Me Workspace (https://github.com/prove2me/prove2me_workspace)

Anthropic, Fermat's Last Theorem in Lean 4 (https://github.com/anthropics/fermats-last-theorem)

Andrej Karpathy, Context engineering (https://x.com/karpathy/status/1937902205765607626)

Aaron Levie, AI agents and professional capability (https://x.com/levie/status/2006521312693637597)