MAESTRO: Agentic Formal Proof Development by Coordination

Summary (Overview)

• MAESTRO is a novel Lean 4 prover harness that replaces local repair of failed proof obligations with global coordination, where a single coordinator oversees the entire proof development process and revises the plan at the level where the problem actually lies.
• The system introduces structured failure diagnoses from workers (provers, planners, explorers, implementers) that report why they failed, not just that they failed, enabling the coordinator to distinguish between insufficient guidance, false lemmas, and flawed decompositions.
• MAESTRO is a unified framework that handles both formal mathematics and verified code synthesis, treating code repair as one more coordinator action within the same feedback loop.
• Empirically, MAESTRO outperforms plain coding agents (Claude Code, Codex) on every benchmark not already saturated, with the largest gains on research-level mathematics: up to 34/48 theorems on arXivLean June 2026 vs. 19 for the native agent.
• The system achieves state-of-the-art results across all shared benchmarks: 669/672 on PutnamBench, 59/60 on Lean-IMO-Bench, 6/6 on IMO 2026, and 75-76/77 on AlgoVeri, beating all published prover systems.

Introduction and Theoretical Foundation

Background and Motivation

Lean is increasingly used to verify mathematical proofs and software produced by LLM agents, but writing formal proofs remains difficult. The authors identify a critical limitation in existing prover systems:

"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."

The key insight is that existing systems cannot distinguish between different failure modes. 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. This can lead to:

• Wasted budget on elaborating a flawed proof direction
• Inability to recognize when a lemma is false
• Failure to notice patterns across sibling branches
• No mechanism to retract and replan flawed subtrees

Theoretical Foundation

The paper is grounded in the observation that proof development is inherently an exploratory, iterative process that mirrors how mathematicians work:

"A proof of a hard theorem starts from a plan, and the plan is a guess. Some of its flaws are visible on paper. Others appear only when the attempt on one step gets stuck in a way that shows the plan itself was wrong. At that point someone has to decide whether to push harder on the step, patch it, or abandon the route that led there."

MAESTRO formalizes this loop with:

• A persistent Lean 4 workspace as the record of what has been proved
• Parallel workers attacking open obligations
• A single coordinator that reads diagnoses and steers the proof until no sorry remains

Methodology

System Architecture

MAESTRO operates on a task defined as a frozen Lean 4 context (imports, definitions, hypotheses), a specification, and optionally an implementation. The system maintains a shared Lean workspace where every conjectured lemma is added (with a proof or a sorry).

Workers

MAESTRO employs four types of workers, each reporting structured evidence:

1. Provers: Attempt to close individual obligations. On failure, they return a diagnosis recording:

   • Approaches tried and why they failed
   • Whether the problem is local (missing helper lemma) or global (fundamental barrier)
   • Suspected counterexamples (checked in Lean)
   • Progress reports at regular intervals with compiling partial-proof snapshots

2. Local Lemma Planners: Decompose obligations that provers cannot close. The process involves:

   • Writing a natural-language proof plan with child lemmas
   • A judge reviewing the plan for plan-level defects (not asking for child proofs)
   • Verifying the decomposition genuinely divides difficulty (not just relocating it)
   • Flagging when multiple plans recreate the same "hard core"

3. Free-form Explorers: Launched when diagnoses give the coordinator no further ideas. They:

   • Work out alternative routes without following the current plan
   • Report blueprints with evidence, or conclude the current plan should be kept
   • Never modify the workspace directly

4. Implementers (for verified code generation): Consist of a coder and a judge:

   • Coder writes the implementation
   • Judge tests it against the formal postcondition
   • Judge rejects code that passes tests but misses required complexity or algorithm

Coordinator

The coordinator is an agentic session running for the entire proof, with two primary roles:

Global Blueprint Mutation: Unlike prior systems that only add to the blueprint, MAESTRO's coordinator can:

• Remove parts of the blueprint as easily as adding them
• Fix multiple problems in a single edit
• Abandon parent conjectures while keeping proved children
• Lift duplicated facts into shared lemmas
• Repair upstream dependencies

Worker Dispatch: The coordinator chooses workers based on evidence:

• Prover when evidence points to a strategy (commits to current route)
• Lemma planner when a step is too large (accepts route, splits step)
• Explorer when the route itself is questionable (questions route entirely)
• Decides when to spend more compute vs. more structure

Asynchronous Pipeline

MAESTRO eliminates rounds and fixed timeouts:

• Workers run asynchronously under generous budgets
• All reports enter a single event queue processed by the coordinator as they arrive
• The coordinator decides when attempts should end based on evidence, not fixed timeouts
• Closed proofs are committed directly; diagnoses go to the coordinator for action

Falsification and Code Repair

MAESTRO treats falsification as a core capability:

• Workers can claim a target is false or that the context lacks needed facts
• Claims are verified in Lean:
  • Trying to prove the negation of the target
  • Building a countermodel (concrete example satisfying hypotheses but violating the target)
  • Only counts if it compiles against the unchanged frozen context
• For mathematics: run ends with machine-checked falsification
• For verification: counterexample sent to implementer; kept lemmas retained, obsolete ones removed

Empirical Validation / Results

Main Results

Table 1: Main results (Problems solved per benchmark; a+b = a proven, b falsified)

Key findings:

• Largest gains on research-level mathematics: 63% average improvement on arXivLean (33→54 theorems across four backbones)
• IMO 2026: All six solved with three backbones; five with Opus 4.8 (vs. one for Claude Code)
• Software benchmarks near saturation: All agents solve all 189 Verina tasks; AlgoVeri gains of 4-7 problems

Comparison with Prior Systems

Table 2: Prior systems as published (context, not controlled comparison)

Notably, with the same backbone (GPT-5.4) as IDS, MAESTRO solves 188/189 Verina and 70/77 AlgoVeri vs. 176 and 65 for IDS—and does so in Lean (kernel-verified) rather than Dafny (SMT-solver-assisted).

Robustness to Reasoning Effort

On IMO 2026 with GPT-5.6 Sol:

• Codex: 0-2 problems at low effort, 3-4 at medium, needs xhigh effort for all six
• MAESTRO: 3-5 at low effort, 5-6 at medium, all six from high effort onward (one level earlier)

Ablation: Decomposition Without Coordination

On FATE-X:

• Plain agent: 77 (Fable 5), 70 (GPT-5.6 Sol)
• Naive decomposition: 76 (Fable 5), 72 (GPT-5.6 Sol)
• MAESTRO: 91 (Fable 5), 84 (GPT-5.6 Sol), plus 6 falsifications each

"The gain therefore comes not from decomposition itself but from coordination that decides when to decompose, when to persist, and when to replan."

Case Studies

1. Abandoning a failing construction (FATE-X Problem 90, Hilbert's 14th problem): MAESTRO traced two failing lemmas to an early wrong choice of plane curve, replaced it in a single revision—discarding 22 lemmas (19 already proved), keeping 6, adding 11—and closed the proof 1.4 hours later.

2. Novel proofs for research-level problems (arXivLean008, Frankl-Wang bound): With web search disabled, MAESTRO produced two self-contained proofs different from the published one and from each other—Opus 5 counts elements over prefixes; Fable 5 compresses the family and bounds it level by level.

3. Proofs catch bugs that tests miss (AlgoVeri push-relabel): The standard algorithm passed all judge tests but violated the specification on graphs with duplicate arcs. The bug surfaced during proof, a counterexample was found, and the code was repaired and proved correct.

Theoretical and Practical Implications

Theoretical Contributions

• Global coordination as a design principle: MAESTRO demonstrates that formal proof development benefits fundamentally from treating failures as evidence to be aggregated across the entire proof structure, rather than as local events to be handled by fixed rules.

• Structured diagnosis as enabling mechanism: The system shows that rich failure information (approaches tried, needed facts, suspected counterexamples) is both feasible to collect and essential for intelligent replanning.

• Unified treatment of mathematics and code verification: By acting on formal obligations rather than domain-specific tactics, the same coordination mechanism handles theorem proving, implementation verification, and code synthesis.

Practical Implications

• Research-level mathematics: The significant gains on arXivLean (34/48 theorems with Opus 5) suggest AI provers can now contribute complementary angles on open research problems, not merely formalize known proofs.

• Verified software development: The push-relabel case study shows that formal verification catches bugs that test-based approaches miss, and that proof failures can guide code repair.

• Transparency and auditability: Every coordinator decision is recorded with its evidence, making the exploration process inspectable—addressing the community's call for openness about failures in AI-assisted mathematics.

• Compute efficiency: MAESTRO reduces reasoning-effort requirements, enabling cheaper, lower-effort models to become reliable provers.

Conclusion

MAESTRO replaces local repair with global coordination in agentic formal proof development, revising proofs at the level evidence calls for. Key takeaways:

1. Global coordination works: The system achieves state-of-the-art results across mathematics and verified coding benchmarks, outperforming all published systems on shared benchmarks.

2. Flexibility is key: The same framework handles mathematical theorems, verification of existing code, and joint code-and-proof synthesis.

3. Research potential: Strong results on recent research theorems suggest potential for research-level mathematics, with run records opening AI prover exploration to inspection and study.

Future directions implied by the work include:

• Scaling to even harder research-level problems
• Further investigation of how coordination patterns affect proof discovery
• Potentially using the recorded exploration histories to train better provers

The authors note that MAESTRO is open source, and every run produces a complete record of its search—conjectured and retracted lemmas, tried and abandoned routes, and the evidence behind each change—making the exploration transparent and available for study.