Maestro: Agentic Formal Proof Development by Coordination
Haoyu Li, Zeren Shui, Yuhao Zhang, Ferhat Erata, Benjamin Mikek, Murali Krishna Ramanathan, Hao Zhou
Strong, timely agentic-prover harness with large gains on research-level Lean benchmarks and a clean coordination-vs-decomposition ablation, tempered by prompt-engineering-heavy novelty and unmatched-compute/uncontrolled cross-system comparisons.
Abstract
Lean is increasingly used to verify mathematical proofs and software produced by LLM agents, but writing formal proofs remains hard. Existing prover systems take a divide-and-conquer approach that recursively decomposes hard proof obligations into easier lemmas and splits again any lemma that resists proof. However, a lemma can resist proof for different reasons, including insufficient guidance, a false statement, or a flaw in the decomposition that produced it. Existing systems cannot tell these apart as a failed attempt reports little beyond its failure, and responses are confined to the failing node without considering the rest of the proof or revising the plan above it. The system may thus keep decomposing obligations along a flawed proof direction until the budget runs out, causing the whole proof attempt to fail. We introduce Maestro, a Lean prover harness that handles failures through global coordination. Provers report why they failed, not just that they failed, and a coordinator that sees the whole proof chooses an appropriate response, such as guiding a stuck prover, correcting a false lemma, or retracting a flawed subtree and replanning it. The same harness extends to verified code synthesis, where a checked counterexample sends the code back for repair. We evaluate Maestro with four frontier LLMs on seven mathematics and three software verification benchmarks. It proves more targets than each model's native coding agent (Claude Code or Codex) on every benchmark the agent has not already saturated, with the largest gains on research-level mathematics. With Claude Opus 5, it discovers its own proofs of 34 of the 48 theorems in the June 2026 release of arXivLean, against 19 for the native agent. It also outperforms all published prover systems on every benchmark they share, solving 669/672 PutnamBench, 59/60 Lean-IMO-Bench, and 6/6 IMO 2026.
AI Impact Assessments
(1 model)Core Contribution
Maestro is an open-source Lean 4 proving harness that replaces the local failure handling of recursive-decomposition provers (Hilbert, LEAP, Goedel-Architect) with global coordination. Workers return structured diagnoses (routes tried, missing facts, checked counterexamples, a local-vs-global scope assessment) instead of a bare failure. A persistent coordinator agent sees the whole workspace. It can retry with guidance, add shared lemmas, restate or falsify targets, retract subtrees while keeping proved lemmas, launch explorer cohorts, and redirect running provers through an asynchronous event queue. Falsification claims are checked in Lean. For verified coding, a checked counterexample is routed back to an implementer to repair the code, with the specification held fixed. Everything is recorded in the workspace, so each run leaves an auditable trace.
The core idea (failure diagnosis plus global plan revision, with decomposition as one action among many) is a sensible and well-motivated architectural step. It is largely an agent-orchestration and prompt-engineering contribution on top of frontier LLMs, not a new learning algorithm or proof technique.
Methodological Rigor
Strengths:
Limitations:
Potential Impact
Timeliness
This is highly timely. Agentic Lean proving with frontier models is where the field is moving, and the decomposition-based pipelines are the incumbent. The paper's argument that local repair is insufficient is well-motivated and matches practitioners' experience.
Strengths & Limitations
Strengths: strong empirical gains on hard benchmarks; a clear ablation separating coordination from decomposition; a cost analysis; open source; interpretable traces; broad benchmark coverage; concrete case studies; benchmark error discovery.
Limitations: most of the coordinator's intelligence lives in long natural-language prompts, so the contribution is hard to separate from the backbone and the prompt engineering. Component-level ablations are missing. Single-seed main results are another weakness. Compute is unmatched. Cross-system comparisons are uncontrolled. The software-verification gains are marginal. Generalization beyond Claude/GPT-class frontier models is untested. The novelty is architectural rather than conceptual: related work such as blueprint refinement and the explorer pattern already partly covers the idea. Reproducibility depends on proprietary models and heavy compute (up to millions of tokens per problem), though the code and prompts are released.
Overall, this is a solid, timely systems paper with strong results that will probably be widely cited as a reference harness. It is less likely to be a conceptual landmark.
Generated Oct 20, 2026
Comparison History (0)
Strong, timely agentic-prover harness with large gains on research-level Lean benchmarks and a clean coordination-vs-decomposition ablation, tempered by prompt-engineering-heavy novelty and unmatched-compute/uncontrolled cross-system comparisons.