The authors design Maestro, a Lean prover harness that uses a single coordinator to oversee multiple worker agents attacking open proof obligations.
Global coordination of proof agents beats local repair in formal theorem proving
Maestro uses a single coordinator to diagnose failures and orchestrate retries, fact addition, or replanning, outperforming prior provers on math and software benchmarks.
Big Tech
Haoyu Li · Zeren Shui · Yuhao Zhang · Ferhat Erata · Benjamin Mikek · Murali Krishna Ramanathan · +1 more
University of Illinois Urbana-Champaign · AWS AI Labs · Georgia Institute of Technology
Research Digest··2 min read
The authors present Maestro, an agentic framework for Lean proof development that replaces local repair of failed subgoals with global coordination.
§