Global Proof Coordination

Sources#

• Maestro: Agentic Formal Proof Development by Coordination

Summary#

Recursive Lean provers (Hilbert, LEAP, Goedel-Architect, DeepSeek-Prover-V2's subgoal decomposition) answer every failed lemma the same way and at the same place: split it again, or repair its statement in place. A lemma can resist proof for three different reasons. The prover needed better guidance, the lemma is false, or the decomposition above it went the wrong way. A failed attempt that reports only "failed" cannot tell these apart. Maestro: Agentic Formal Proof Development by Coordination (Haoyu Li, Zeren Shui, Yuhao Zhang, Ferhat Erata, Benjamin Mikek, Murali Krishna Ramanathan, Hao Zhou; UIUC, AWS AI Labs, Georgia Tech; arXiv 2610.25920, 2026-10-19, empirical) builds the alternative and names it global coordination instead of local repair. Workers report why they failed. A single persistent coordinator reads every report and edits the shared Lean workspace at whatever level the evidence points to, and that includes deleting lemmas that are already proved.

The paper's results are self-reported. Its strongest datum is an ablation, not a headline. A decompose-and-judge baseline built on the same backbones, with no coordinator, scores about the same as the plain coding agent on FATE-X: 76 against 77 on Claude Fable 5, 72 against 70 on GPT-5.6 Sol. Maestro scores 91 and 84 and falsifies six more targets in each case. Decomposition alone is not the gain. The gain is deciding when to decompose, when to persist, and when to replan.

The design#

Four worker types, each trusting the current plan to a different degree. Provers commit to the current route. Local lemma planners accept the route but split one step. Each is a proposer, then a judge that rejects a plan if one child is as hard as its parent, then a translator into Lean sorry stubs. Free-form explorers work in private copies of the workspace, may ignore the incumbent plan, and return a candidate blueprint as evidence. They never publish proof text directly. Implementers, used for verified code, pair a coder with a judge that tests the output against the formal postcondition. Choosing which worker to send is itself a judgment about the plan.

The diagnosis is the interface. A failing prover returns a verdict block. It holds an outcome (stuck_hard, suspect_false with a Lean-checked witness, need_stronger_hyp, blocked_env), a failure_scope of local, global or uncertain, a structural_need (local lemma, stronger interface, representation change, upstream rearchitecture), and a repair_target naming the responsible ancestor. Long-running provers also send heartbeats with a compiling snapshot and a 0–100 closeness estimate. This is what lets the coordinator see patterns no single node shows: siblings failing for want of the same fact, or repeated decompositions recreating the parent's hard core.

Blueprint mutation in both directions. Most pipelines only add to the blueprint. Maestro's coordinator submits atomic, compile-checked edits that can RETRACT a body to sorry, ABANDON a declaration and repair its consumers, RESTATE, ADD_HELPER once for several branches, or rebuild from the root. One objective criterion constrains every edit: the workspace compiles and the frozen statements are intact. Its prompt (Appendix E.1) names the coordinator's most dangerous failure mode as "overconfidence in scaffolding that you helped create". It lists signs that the problem lies above the current node: the same hard residual surviving different attempts, three or four helper levels without real reduction, one kernel staying as hard as its parent while its siblings close. It says to judge progress "by mathematical leverage, not activity, tree size, or sorry count". Explorer cohorts (1, 5, 10 or 15) are "raw material for your reasoning, not a ballot … never choose by majority vote".

No rounds, no fixed timeouts. Workers run asynchronously under a generous budget into one event queue. Closed proofs commit directly, and diagnoses go to the coordinator. A round-based pipeline needs a per-worker timeout, and any fixed value either stalls every round on its slowest worker or kills provers that were close and replaces their work with a fresh decomposition.

Falsification is checked, not trusted. A "this target is false" claim counts only if a proof of the negation or a countermodel compiles against the unchanged frozen context. A "the context lacks a fact" claim is rejected if the fact can be proved from the context. An unsupported claim is reported as unverified. In verified coding a confirmed counterexample goes to the implementer as a bug report. Once the code changes, the coordinator keeps the lemmas that still hold and drops the ones tied to the old code.

Results (Tables 1–2, reconciled against pdftotext -layout)#

Four backbones (Claude Opus 4.8, Opus 5, Fable 5, GPT-5.6 Sol), all at high reasoning effort. Each runs as a plain coding agent with Lean skills (Claude Code or Codex) and as Maestro's backbone. The tools are the same throughout (shell, a Lean MCP server, a local Loogle), web access is disabled, and Table 1 is one rollout per task.

• The margin grows with difficulty. Averaged over backbones, the two arXivLean releases (89 theorems from recent papers) go from 33 to 54, +63%, ranging from +43% (Sol) to +79% (Opus 5). With Opus 5 on the June release it is 34 against 19, the abstract's headline. Verina is saturated by every plain agent, and NTP4VC differs by at most one proved task. On NTP4VC, Fable 5's Maestro run proves one fewer task than its plain agent (588 against 589) while falsifying 11. So "beats the plain agent on every unsaturated benchmark" holds only if NTP4VC is read as saturated.
• Repeated runs (Appendix B, Figure 5). On the four hardest benchmarks, with Fable 5 and Sol, the weakest Maestro run beats the strongest plain run every time. FATE-X means are 92.3 against 78.7 (Fable) and 84.3 against 66 (Sol). The caption says "two or three runs" while the prose says three. A mean of 34.5 implies two runs for at least one configuration.
• Reasoning effort (Figure 2, IMO 2026, Sol, three runs per setting). Plain Codex solves 0–2 at low effort, 3–4 at medium, and needs xhigh to solve all six every time. Maestro solves 3–5 at low, 5–6 at medium, and all six every run from high upward.
• Against published systems (Table 2, explicitly not controlled). PutnamBench 663–669 against 597 for Goedel-Architect, Lean-IMO-Bench 57–59 against 42 for LEAP, AlgoVeri 75–76 against 65 for IDS. The one same-model pair is GPT-5.4, IDS's backbone: Verina 188 against 176, AlgoVeri 70 against 65, and IDS works in Dafny, where an SMT solver discharges most obligations.

Cost (Appendix A, FATE-X only). Problems are binned by how many of three plain runs solve them, and medians are taken over problems Maestro solves. Easy: about one plain run's cost (113K against 96K output tokens on Fable, 20K against 24K on Sol). Medium: a single Maestro run solves 11/11 and 9/10, at less than three plain runs combined (482K against 543K, 173K against 240K). Hard, where no plain run succeeds: 9/16 and 14/28 proved, at medians of 2.0M and 872K. The cost grows with difficulty. This is the paper's case that coordination is better targeted test-time compute than repeated sampling (Large-Scale Test-Time Compute). It holds only on FATE-X and only on problems Maestro solves. Table 1 itself is not compute-matched.

Three case studies from the run records#

• Discarding proved work decides the outcome. FATE-X Problem 90 asks for a counterexample to Hilbert's fourteenth problem. Both the decompose-only baseline and Maestro (Fable 5) began from a plane curve that did not work. The baseline kept splitting below it until it gave up. Maestro's coordinator traced two failing lemmas back to the choice of curve. In one edit it discarded 22 lemmas, 19 of them already proved, kept the 6 that did not depend on the curve, and added 11 for a simpler one. The proof closed 1.4 hours later. A pipeline that only grows its plan cannot make this move.
• Proofs that differ from the published one. ArxivLean008 is Frankl and Wang's bound on 3-wise t-intersecting families. Every plain agent and every system on the public leaderboard fails on it. Its published proof uses two theorems missing from Mathlib. Maestro proves it with two backbones, and each argument is self-contained: Opus 5 counts over prefixes, Fable 5 compresses and bounds level by level. Neither resembles the published proof or the other. The authors claim "complementary angles", not better proofs. With web search off and arXiv-sourced targets, contamination of the statement is possible, but a proof unlike the published one argues against retrieval of the proof itself.
• Proofs catch what tests miss. AlgoVeri's push-relabel specification treats a doubly-listed arc differently from the textbook definition. Opus 5's and Fable 5's standard implementations passed every judge test. A proof obligation then failed, a worker built a graph on which the code violates its specification, and the coordinator blamed the code rather than the proof. With Opus 5 the repaired code was proved.

The longest development: the June release's problem 5, a volume lower bound for 3-D constant-width bodies. Only Fable 5 under Maestro proved it, in 7.4 hours, across 17 files and 7,584 lines, including a small theory of harmonic polynomials built from scratch.

Falsified benchmark targets#

Maestro falsified 22 targets with compiling Lean certificates: 2 in PutnamBench, 1 in Lean-IMO-Bench, 2 in arXivLean June, 6 in FATE-X and 11 in NTP4VC. Most are misformalizations. Irrational (f 1/2) parses as f(1)/2 (Putnam 2017 B3). ¬ IsField R also excludes non-commutative rings, so the quaternions break FATE-X 13. A matrix written as a function makes ^ k entrywise (ArxivLean023). Nine of NTP4VC's eleven are Why3-to-Lean translation errors. A smaller set is faithful to the wording and false in the mathematics: FATE-X 74, 75 and 86, and ArxivLean037, which is "wrong already in the source paper" (the Fano plane has seven edges at k = 8). The authors report that arXivLean's maintainers later removed both falsified arXivLean targets. That is an external confirmation, though it comes second-hand through the authors. This is Statement Drift surfaced by search. When the system is allowed to answer "false" with a certificate, it becomes a benchmark auditor.

How much to believe#

• Self-built, self-baselined. The authors built Maestro, ran every plain-agent arm, and built the decompose-only ablation themselves. Five of the seven authors are at AWS AI Labs. No vendor COI applies to the models compared (Anthropic and OpenAI backbones). Prompts are published in full (Appendix E) and the harness is stated to be open source.
• Not compute-matched where it matters most. Table 1 is one rollout per arm with no token figures, and Maestro spends more on hard problems by design. The only cost comparison is FATE-X medians over Maestro-solved problems, so the research-level arXivLean margin has no cost denominator.
• Axiom audit reported for three developments only. Lean reports that the Appendix D root theorems depend only on propext, Classical.choice and Quot.sound. The prompts forbid axiom/opaque/constant, and success is defined as "compiles and the frozen statements are intact". The paper does not say that every counted benchmark solve was checked against a whitelist or Comparator, so the headline counts sit at the level Kernel-Level Proof Auditing asks to be audited.
• The ablation is narrow. One benchmark (FATE-X), two backbones, one run, and the coordinator's components (diagnosis schema, global mutation, asynchrony, explorers) are never removed one at a time. "The gain comes from coordination" is supported against decomposition. Which part of coordination carries it is not measured.
• Benchmark freshness. IMO 2026 is n = 6, and Codex with Sol already solves it. PutnamBench and Lean-IMO-Bench are near ceiling for both arms. The discriminating evidence is arXivLean, FormalQualBench and FATE-X.

Where it sits#

• Against the loop-versus-bespoke ledger (Agentic Loops Overtake Bespoke Systems). This is a bespoke harness beating a stock frontier coding agent on the same model, which the mini-Lean-agent result (bash-only beating Lean-tooled AxProverBase) and the MLE plain-loop result had made look unlikely at frontier backbones. Two things reconcile them. The margin is concentrated on research-level problems, the receding hard frontier that page predicts. And the structure that pays is coordination, not tooling affordance. The ablation also bears on ProofEvolve's reproduction, where Hilbert- and LEAP-style decomposition beat a ReAct loop by 20–25 points. Here the same design over Claude Code / Codex sessions adds roughly nothing. That fits the MLE paper's reading that search machinery designed for single completions is redundant once each node is a full agent session.
• Against verified block decomposition (Verified Block Decomposition for Agent Teams). Both put a coordinator between local workers and a global verifier, and both say a check that only rejects is not enough. Ilin and Richtárik's correction tells an agent which alternative to try. Maestro's diagnosis tells the coordinator at which level to act. Maestro adds what the block theory excludes by assumption: rewriting the block structure itself mid-run.
• Against the council branch (Many-Agent Proof Harnesses). Same many-worker shape, but the grader is the kernel, and this paper publishes the matched plain-agent arm and a decomposition ablation that Stellar Colosseum and the Navier–Stokes apparatus do not.
• Against self-built harnesses (The Harness Adaptation Gap). Human-designed harnesses beat a generic Claude Code baseline by wide margins on ARC-AGI-3 (Schema 42.83 against 98.98). Maestro is the formal-math instance of the same human-steered headroom, with a kernel instead of a game score.
• For the field's search-variance question (AI-Driven Formal Proof Search). The repeated-runs figure is the corpus's first frontier-model evidence that a harness change moves the reachable set by more than run-to-run spread on research-level Lean targets.

Connections#

• Agentic Loops Overtake Bespoke Systems — the ledger this result lands in: a same-model bespoke-over-stock-agent win at frontier backbones, concentrated at the hard end, and an ablation showing decomposition without coordination ties the plain loop
• AI-Driven Formal Proof Search — the paradigm; Maestro is a kernel-grounded proving harness whose run records expose the search, and its repeated-runs data bears on that page's reachability question
• Many-Agent Proof Harnesses — the many-agent formal harness with the controls the council branch lacks: a plain-agent arm on every backbone and a coordinator ablation
• Statement Drift — 22 benchmark targets falsified with compiled certificates, most misformalizations and a few faithful-but-false source claims
• Kernel-Level Proof Auditing — the audit the headline counts have not been given: axiom dependencies reported for three showcased developments, not for every counted solve
• Verified Block Decomposition for Agent Teams — the theory sibling: coordinator plus exact verifier over local workers, where Maestro also lets the coordinator rewrite the decomposition
• The Harness Adaptation Gap — the same human-designed-harness headroom over a generic Claude Code baseline, in a kernel-verified domain
• Large-Scale Test-Time Compute (hub) — coordination as targeted test-time compute: cost grows with difficulty, and on medium FATE-X problems one run beats three plain runs at fewer tokens
• Verification as the New Bottleneck (hub) — proofs as a bug-finder that tests miss (push-relabel), and the coordinator's job as deciding what a failed check means
• Lean, Claude Code, Codex, Claude Opus 5, Claude Fable 5 — the verifier, the two plain-agent baselines, and two of the four backbones
• Library-Grade Formalization — the library-scale counterpart: coordinated agent swarms (Tau Ceti, Formal Frontier) scored by whether others can build on the output rather than by solves

Open Questions#

• Does the research-level margin survive a compute match? Table 1 has no token counts, and the only cost comparison is FATE-X medians over Maestro-solved problems. Settler: arXivLean (March and June) run with plain-agent best-of-k at the same total output tokens as one Maestro run, per backbone, counting all problems rather than only solved ones.
• Which part of coordination carries the gain? The ablation removes the coordinator entirely. Settler: a FATE-X or arXivLean ablation that keeps the coordinator but removes one component at a time: structured diagnoses (bare failure only), destructive edits (no RETRACT/ABANDON), asynchrony (fixed rounds), or explorers.

Sources#

• Maestro: Agentic Formal Proof Development by Coordination — Li, Shui, Zhang, Erata, Mikek, Ramanathan & Zhou (UIUC; AWS AI Labs; Georgia Tech), arXiv 2610.25920, 2026-10-19, 43 pp including appendices A–E, empirical. Table parse note: PDF-derived (docling 2.126.0 / docling-mlx 0.1.1). Table 1 renders each model's two arms as space-joined pairs in one cell ("587 663+2"), and Tables 1 and 2 were reconciled cell by cell against pdftotext -layout on before the table above was written. They match. The Appendix D.3 file-listing table is welded (ten filenames and their descriptions in one cell, lines orphaned in fragment rows) and is cited only for the prose totals (17 files, 7,584 lines). Figures 2–5 were not opened. Every figure-derived number is from the prose. Self-reported on the authors' own system, with baselines run by the authors