Maestro: Agentic Formal Proof Development by Coordination
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...
| Authors | Haoyu Li, Zeren Shui, Yuhao Zhang et al. |
|---|---|
| Primary category | cs.LG |
| Published | 19 October 2026 |
| Last updated at source | 19 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 20 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.