Source-linked AI summary
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
Jules Viennot, Guillaume Baudart, Marc Lelarge
TL;DR
Proof-assistant interfaces shape agent interaction, yet existing interfaces were designed for human users. This paper evolves a Rocq server by retaining features that improve smaller models, and reports gains over two comparison servers across four models on held-out miniF2F-Rocq; a Lean port improves cost and time per solve on a PutnamBench subset.
Problem
Proof-assistant interfaces adapted from human-oriented tools are not optimized for agents, despite shaping what agents receive and the cost of their interactions.
Source: §1 · p. 2Method
A frontier model incrementally proposes interface features, retaining those that improve smaller models, to grow ROCQ-MCP-EVOLVE from a compiler-only server.
Source: §2 · p. 3Results
Takeaways & Limitations
The Lean port improves cost and time per solve on a subset of PutnamBench, while the paper identifies growing a Lean server from a compiler-only baseline as future work.
Source: §1 · p. 2, §6 · p. 9On a subset of PutnamBench, LEAN-MCP-EVOLVE improves cost and time per solve but its solve rate remains below LEAN-LSP-MCP.
Source: §6 · p. 9
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Proof assistants provide machine-checked validation for AI-generated proofs, but agents interact with them through interfaces adapted from human tools. The paper evolves an agent-facing Rocq interface and reports improved results across models and tasks.
1 INTRODUCTION
- Proof assistants can validate generated proofs with machine-checked certificates, but producing them requires intensive agent–prover interaction.Source: §1 · p. 2
- Existing proof-assistant interfaces, often MCP servers, were adapted from human-oriented systems and are not optimized for agents, although they shape interaction costs.Source: §1 · p. 2
- A frontier model incrementally proposes interface features and retains those that improve smaller models’ performance on curated problems.The authors evaluate on mathematical and project-scale tasks and present an evolutionary method, ROCQ-MCP-EVOLVE, and an evaluation across model sizes and families.Source: §1 · p. 2
- ROCQ-MCP-EVOLVE outperforms CONTROL and ROCQ-MCP in success rate, cost per solve, and time per solve across four models on the held-out miniF2F-Rocq test split.The paper also reports the same ordering on project-scale tasks; its Lean port improves cost and wall time per solve, though its solve rate is lower than LEAN-LSP-MCP.Source: §1 · p. 2
2 THE EVOLUTIONARY PROCESS
The process starts with a compiler-only server, then iteratively tests model-proposed changes on curated tasks. Separate validation procedures govern mathematical exercises and project-scale tasks, while an anti-cheating system checks reported successes.
2 THE EVOLUTIONARY PROCESS
- A frontier-model orchestrator mutates a compiler-only server, evaluates each version with smaller-model testers, and validates or discards changes based on measured added value.The process is iterative, with the orchestrator consulting prior-run statistics and logs; human involvement is limited to setting objectives, budgets, validation rules, and daily review.Source: §2 · p. 3
2.1 PHASE 1: SOLVING MATHEMATICAL EXERCISES
- Phase 1 tests mathematical exercises under fixed time and call budgets, using dev60 and additional datasets for mutations that require broader or specialized evaluation.dev60 contains 60 Rocq Workbook problems across three difficulty buckets; other datasets target difficult problems, MathComp-specific features, or automation on miniF2F-Rocq. Mutations are accepted by per-bucket success thresholds, with cost and wall time secondary.Source: §2.1 · pp. 3–4
2.2 PHASE 2: PROJECT-SCALE TASKS
- Phase 2 tests five multi-file autoformalization projects, while file-handling tools are supplied separately and excluded from mutation evaluation.The projects cover mathematics and computer science and include test suites; mutations are accepted or reverted by success-count thresholds, with cost or wall-time reductions relevant when success differences are small.Source: §2.2 · p. 4
2.3 ANTI-CHEATING SYSTEM
- An anti-cheating system checks proofs for edits to protected file prefixes, forbidden proof shortcuts, and extra imports, then recompiles in isolation and audits assumptions.For projects, it rebuilds in an isolated directory, compiles the test suite, and audits assumptions on each test.Source: §2.3 · pp. 4–5
3 ROCQ-MCP-EVOLVE
ROCQ-MCP-EVOLVE combines a live interactive Rocq session with proof-state, tactic, automation, and verification tools. Its evolution improved dev60 accuracy, while selected mutations exposed both useful features and limits of the evaluation process.
3 ROCQ-MCP-EVOLVE
- A live interactive session preserves proof progress between calls; the server also supports tactics, backtracking, proof-state access, automation, and proof or project verification.A Rocq call takes about 1 ms with the session mechanism, compared with 266 ms for full compilation.Source: §3 · p. 5
- .33 to .54: accuracy on dev60 difficulty buckets rose across accepted Phase 1 mutations, and the final server solved more attempts than CONTROL on 22 problems and fewer on none.Cost and wall time were not used to validate Phase 1 mutations, but both improved in the final server compared with CONTROL.Source: §3 · p. 5
- Several specialized mutations were rejected; preloaded automation addressed an anti-cheating constraint, and the false-winner fix corrected auto close reporting success without tactic progress.Team collaboration and two MathComp-specific mutations were rejected; the false-winner fix is listed separately from the following iteration.Source: §3 · pp. 5–6
- The search tool was heavily used but produced no accuracy gain, while Phase 2 mutations were rejected and the orchestrator stopped at a local optimum before exhausting its budget.Phase 2 ended at $116 of the $150 budget.Source: §3 · p. 6
4 EVALUATION
Across four models, the evaluation compares ROCQ-MCP-EVOLVE with a compiler-only baseline and an established MCP server, then tests project-scale use, transfer to Lean, and the role of automation. The results cover benchmark accuracy, cost, and wall time, with a separate Lean comparison on putnam60.
4.1 MINIF2F-ROCQ
- At least +30 points in accuracy over CONTROL on every model; ROCQ-MCP-EVOLVE also beats both servers across all miniF2F-Rocq difficulty buckets.It beats ROCQ-MCP on more attempts than it loses, and results with GPT-5.6 Terra are similar to Opus.Source: Table 2 · p. 7, §4.1 · p. 7
- ROCQ-MCP-EVOLVE uses the fewest calls, cuts input tokens by 24% and output tokens by four versus CONTROL, lowering cost and wall time.The efficiency comparison covers problems solved by all three servers in at least one run.Source: §4.1 · p. 7, Table 3 · p. 8
4.2 RQ1: ARE TOOLS EVOLVED ON EXERCISES USEFUL FOR BUILDING ENTIRE PROJECTS?
- On project tasks, ROCQ-MCP-EVOLVE leads all three metrics; accuracy gains over CONTROL are +20 points (Sonnet), +30 (Opus), and +10 (Terra).Cost falls 8%, 14%, and 27%, and wall time 29%, 20%, and 19% for Sonnet, Opus, and Terra, respectively, versus CONTROL.Source: Table 4 · p. 8, §4.2 · p. 8
4.3 RQ2: DO RESULTS TRANSFER TO ANOTHER PROOF ASSISTANT?
- On putnam60, LEAN-LSP-MCP leads accuracy, while LEAN-MCP-EVOLVE leads cost and wall time; LEAN-MCP-EVOLVE and CONTROL tie on accuracy.The authors cannot rule out Sonnet contamination on PutnamBench or prior training on LEAN-LSP-MCP.Source: §4.3 · p. 8, Table 5 · p. 9
4.4 RQ3: HOW MUCH OF THE GAINS COME FROM STANDARD AUTOMATION?
- Auto-close solves 52/244 miniF2F-Rocq problems (21%; easy/medium/hard rates .35/.06/.03), but does not explain the server's full performance gains.On those problems, ROCQ-MCP-EVOLVE averages $0.03 and 11 s per solve, versus $0.06 and 19 s with ROCQ-MCP.Source: §4.4 · p. 9
5 RELATED WORK
Prior proof-assistant interfaces were not designed through an iterative process that measures the value of individual tools. This work instead positions prover-specific tool evolution alongside broader efforts to evolve agent tools and harnesses.
Agent/Prover interfaces
- Existing Lean interfaces emphasize speed, robustness, and scalability, but none known to the authors used evolutionary design to optimize tool selection.ROCQ-MCP was designed by a frontier model but did not measure each tool’s added value, was limited to one iteration, and was not rigorously evaluated.Source: §5 · p. 9
Evolving interfaces
- Unlike task-specific tool libraries or evolving whole agent harnesses, this process evolves one prover-specific feature at a time.The authors distinguish their focus from self-modifying Lean proof agents that optimize proof repair and focus on standalone miniF2F theorems; their tools target project-scale tasks.Source: §5 · p. 9
- Across model sizes and families, the authors report gains on three metrics, while related approaches evolve reusable tools, runtime MCP tools, or proof-agent harnesses.RocqSmith instead optimizes prompts and control flow for Rocq.Source: §5 · p. 9
6 CONCLUSION AND FUTURE WORK
The paper concludes that evolutionary interface design produced a Rocq server that outperforms two alternatives on held-out miniF2F-Rocq and project-scale tasks. It also identifies Lean-specific evolution as a next step and documents AI use, review, and reproducibility.
6 CONCLUSION AND FUTURE WORK
- ROCQ-MCP-EVOLVE beats CONTROL and ROCQ-MCP in success rate, cost per solve, and time per solve on held-out miniF2F-Rocq and project-scale tasks.Although mutations were validated only on accuracy, tight tester budgets reduced calls and tokens, which translated into lower cost and wall time on every tested model.Source: §6 · p. 9
- A Lean-specific evolutionary process remains future work; the existing port improves cost and time per solve on a PutnamBench subset but has lower solve rate than LEAN-LSP-MCP.Growing a Lean server from compiler-only CONTROL would test which evolved features generalize across proof assistants and which are Rocq-specific.Source: §6 · p. 9
Required disclosures
- The authors designed the evolutionary method, objectives, validation rules, and anti-cheating protocol, while the orchestrator proposed, implemented, evaluated, and judged server mutations.Generative AI also contributed to experiments, hypotheses, interpretation, synthetic project datasets, and dataset cleaning; authors reviewed the work and decision trail.Source: AI USE STATEMENT · p. 10
Recommended disclosures
- The manuscript was written by the authors, with AI assistance for code, an initial technical report, readability edits, and related-literature search and summaries.The technical report drew on the orchestrator’s logs and was used as a source of facts alongside raw logs.Source: AI USE STATEMENT · p. 10
REPRODUCIBILITY STATEMENT
- The evolutionary outcome cannot be replayed deterministically, but its mutations, evaluations, and verdicts are documented for audit.The released server is the frozen result of that chronology; the process and evaluation protocol, datasets, and results are described across the paper and appendices.Source: REPRODUCIBILITY STATEMENT · p. 10
- Most results aggregate two to four runs per problem, and cost and wall time are compared on attempts solved by all servers.The number of runs is reported with each experiment.Source: REPRODUCIBILITY STATEMENT · p. 11