# Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean

arXiv: https://arxiv.org/abs/2609.39544 · HTML: https://mlsanity.com/paper/2609.39544/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 19 of its 31 references that are in the map.
- First posted on arXiv 30 Sep 2026.

## Builds on (most cited first, 19 of 19)

- [Voyager: An Open-Ended Embodied Agent with Large Language Models](https://mlsanity.com/paper/2305.16291/) (2023)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Darwin Godel Machine: Open-Ended Evolution of Self-Improving Agents](https://mlsanity.com/paper/2505.22954/) (2025)
- [Meta-Harness: End-to-End Optimization of Model Harnesses](https://mlsanity.com/paper/2603.28052/) (2026)
- [Large Language Models as Tool Makers](https://mlsanity.com/paper/2305.17126/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Agentic Harness Engineering: Observability-Driven Automatic Evolution of Coding-Agent Harnesses](https://mlsanity.com/paper/2604.25850/) (2026)
- [A Self-Improving Coding Agent](https://mlsanity.com/paper/2504.15228/) (2025)
- [TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Tasks](https://mlsanity.com/paper/2401.12869/) (2024)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study](https://mlsanity.com/paper/2503.04763/) (2025)
- [AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities](https://mlsanity.com/paper/2606.26442/) (2026)
- [The Devil Is in the Interface: Evaluating How Tool Architecture Shapes Coding Agent Behavior](https://mlsanity.com/paper/2608.11386/) (2026)
- [AI-Assisted Completion of CertiGC Proofs: An Experience Report](https://mlsanity.com/paper/2606.21167/) (2026)
- [Is Bash All You Need? An Empirical Study of Tool Interfaces for Enterprise Digital Worker Agents](https://mlsanity.com/paper/2609.11999/) (2026)
- [RocqSmith: Can Automatic Optimization Forge Better Proof Agents?](https://mlsanity.com/paper/2602.05762/) (2026)
- [Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution](https://mlsanity.com/paper/2607.17352/) (2026)

## Abstract (arXiv)

Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what the agent receives from the prover and the cost of these interactions. Today, these interfaces are adapted from tools designed for humans and not optimized for agents. We propose an evolutionary method where a frontier model incrementally proposes new features and only keeps the ones that improve the overall performance of smaller models. We demonstrate the effectiveness of our method by growing, on a curated set of mathematical problems, ROCQ-MCP-EVOLVE, a new MCP server for the Rocq prover. On the held-out test split of miniF2F-Rocq, an agent equipped with ROCQ-MCP-EVOLVE outperforms both the baseline that only exposes the Rocq compiler and an established MCP server, across four models from two families, in success rate, cost per solve, and time per solve. Although evolved for Rocq, the resulting server transfers to Lean, improving cost and time per solve on a subset of PutnamBench. We release ROCQ-MCP-EVOLVE and its port to Lean.