cs.AISep 30, 2026
SaveGrowing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
Organizations: IRIF, Universit´e Paris Cit´e, Inria, CNRS · DI ENS, PSL University, Inria
Abstract
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, \rme, a new MCP server for the Rocq prover. On the held-out \texttt{test} split of miniF2F-Rocq, an agent equipped with \rme 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 \rme and its port to Lean.
Figures & tables
Figure 1: Results on the test split of miniF2F-Rocq. Each model is evaluated with three MCP servers: control , a minimal server wrapping the Rocq compiler, rocq-mcp , an established MCP server for Rocq, and rocq-mcp-evolve . For a fair comparison, cost and wall time are averaged over the theorems proved with all three servers.
Figure 2: A step of the evolutionary process. The mutation designed by the orchestrator is denoted by the dark red color. The purple dotted box represents rocq-mcp-evolve , the blue dotted box represents the evaluation of the mutation. The light gray circle shows the process is iterative: a new step starts at the end of the previous one.
Figure 3: Evolution of accuracy, cost, and wall time across both phases. In the left column, the mutations are numbered chronologically and correspond to x-axis labels. Numbers 0 and 15 are not mutations but the starting servers of the phases. Colors indicate the dataset each point was measured on. Each mutation is linked to the version it is compared to. The link of a reverted mutation is dotted, its background is gray and its data point is a cross. The background of a bug fix is hatched gray.
Table 1: Detailed results of the evolution process. Each line corresponds to a mutation of Table 8 . Each cell reports the change with respect to the previous version as a diff: the number of new successes ( ) and failures ( ). For each dataset we report the number of problems in each difficulty bucket, and the number of runs per problem. Phase 1 and Phase 2 are separated by bolder lines. Gray lines indicate reverted mutations. The hatched line is a bug fix (kept).
| Models | MCP servers | Accuracy | Cost ($) | Wall time (s) | |||
| control | .17 | (.28 / .05 / .01) | .07 | (.06 / .07 / .15) | 52 | (50 / 60 / 86) | |
| rocq-mcp | .33 | (.54 / .11 / .07) | .05 | (.05 / .05 / .06) | 32 | (32 / 30 / 48) | |
| Haiku (40 / 4 / 1) | rocq-mcp-evolve | .48 | ( .69 / .30 / .14 ) | .04 | ( .04 / .03 / .05 ) | 19 | ( 19 / 16 / 36 ) |
| control | .50 | (.68 / .35 / .17) | .24 | (.19 / .36 / .39) | 96 | (76 / 153 / 153) | |
| rocq-mcp | .72 | (.88 / .53 / .56) | .16 | (.12 / .28 / .23) | 44 | (30 / 86 / 64 ) | |
| Sonnet (90 / 28 / 7) | rocq-mcp-evolve | .80 | ( .91 / .68 / .67 ) | .11 | ( .08 / .18 / .22 ) | 35 | ( 23 / 62 / 77) |
Table 2: Results on the test split of miniF2F: total (easy/medium/hard). For each model, the cost and wall time are only computed on attempts on the subset of problems solved by all three MCP servers in at least one run (results on the entire dataset are reported in Table 9 of the appendix). The size of this subset per difficulty bucket is given under the model name.
| MCP servers | Calls | Input tokens | Output tokens | Output tokens per call |
| control | 5.9 | 79.0k | 6.6k | 1.12k |
| rocq-mcp | 7.2 | 148.4k | 2.7k | 0.38k |
| rocq-mcp-evolve | 5.6 | 59.9k | 1.6k | 0.29k |
Table 3: Efficiency results for the different MCP servers, averaged over the four models.
| MCP servers | Accuracy | Cost ($) | Wall time (s) | ||||||
| control | .50 | .30 | .40 | 1.56 | 2.19 | 0.22 | 608 | 714 | 332 |
| rocq-mcp | .60 | .60 | .35 | 2.63 | 2.48 | 0.34 | 595 | 661 | 502 |
| rocq-mcp-evolve | .70 | .60 | .50 | 1.44 | 1.89 | 0.16 | 429 | 574 | 269 |
Table 4: Results on project-scale tasks for the models Sonnet Opus Terra averaged on all tasks (detailed results are reported in Table 11 of the appendix).
| MCP servers | Accuracy | Cost ($) | Wall time (s) | |||
| control | .33 | (.93 / .05 / .00) | .12 | (.11 / .28 / –) | 82 | (76 / 183 / –) |
| lean-lsp-mcp | .42 | ( .95 / .30 / .00) | .14 | (.11 / .40 / –) | 86 | (72 / 199 / –) |
| lean-mcp-evolve | .33 | (.83 / .18 / .00) | .11 | ( .09 / .35 / –) | 64 | ( 55 / 159 / –) |
Table 5: Results on putnam60 with Sonnet in Lean for the three MCP servers. Cost and wall time are averaged over problems solved by all three MCP servers in at least one run (16 easy problems, 2 medium problems, and no hard problems).
Appendix figures & tables9 assets
Supplementary material from the paper’s appendix.
Appendix
| Task | Files | Description |
| frugal | 4 | bounded min-plus cost algebra on option nat with a matrix product; laws of the operations and associativity of the product |
| gauges | 4 | closed real intervals over an abstract realType with a sound interval arithmetic; three soundness lemmas and three width lemmas |
| ledger | 4 | append-only ledger of signed deltas with replay and checkpoints; replay/checkpoint equivalence and a bound on balances |
| prodauto | 6 | deterministic finite automata over a finite type; product and complement constructions, language intersection, emptiness by bounded reachability, a pigeonhole pumping lemma |
| triadic | 4 | a divisor-combinatorics dynamical system on natural numbers (from an IMO 2025 problem); a fixed-point theorem and a shrinking theorem |
Table 6: The five project-scale tasks. Each task requires the creation of multiple files on top of the MathComp library.
| rocq-mcp-evolve | rocq-mcp | |
| implementation | OCaml | Python |
| first-party source | 3 527 lines (7 files) | 7 351 lines (8 files) |
| installed components | server + multi-agent daemon/shim | server |
| direct dependencies | 4 opam packages | 3 PyPI packages + coq-lsp toolchain |
| prover attachment | rocq-runtime linked in-process | petanque (coq-lsp) protocol |
| runtime topology | one OS process | server + petanque subprocess; coqc per compile |
Table 7: Implementation . rocq-mcp is implemented on top of a mature software stack developed for IDE support and exposes capabilities this benchmark does not exercise (file outlines, notation resolution, operational diagnostics). rocq-mcp-evolve is implemented on top of the Rocq API.
Table 8: Mutations proposed during the evolution process. Phase 1, the inter-phase, and Phase 2 are separated by bolder lines. Gray lines indicate reverted mutations. The hatched line is a bug fix (kept). accepted, reverted, added without evaluation. The exposed tools are written in this font .
| Models | MCP servers | Accuracy | Cost ($) | Wall time (s) | |||
| control | .17 | (.28 / .05 / .01) | .07 | ( .07 / .07 / .15 ) | 54 | (53 / 60 / 86 ) | |
| Haiku | rocq-mcp | .33 | (.54 / .11 / .07) | .10 | (.09 / .12 / .17) | 54 | (51 / 66 / 96) |
| rocq-mcp-evolve | .48 | ( .69 / .30 / .14 ) | .13 | (.10 / .24 / .23) | 67 | (51 / 116 / 136) | |
| control | .50 | (.68 / .35 / .17) | .25 | (.20 / .38 / .39) | 100 | (77 / 161 / 153) | |
| Sonnet | rocq-mcp | .72 | (.88 / .53 / .56) | .25 | (.17 / .36 / .46) | 73 | (47 / 114 / 142) |
| rocq-mcp-evolve | .80 | ( .91 / .68 / .67 ) | .21 | ( .13 / .33 / .37 ) | 72 | ( 41 / 115 / 127 ) | |
Table 9: Results on the test split of miniF2F-Rocq with cost and wall time computed on the whole dataset instead of the problems solved with all three MCP servers.
| Models | MCP servers | Run | Accuracy | Cost ($) | Wall time (s) | |||
| control | 1 | .17 | (.28 / .05 / .03) | .06 | (.06 / .07 / .15) | 51 | (49 / 64 / 86) | |
| 2 | .17 | (.29 / .05 / .00) | .07 | (.07 / .08 / –) | 52 | (52 / 56 / –) | ||
| rocq-mcp | 1 | .34 | (.55 / .10 / .09) | .05 | (.05 / .04 / .05) | 32 | (32 / 33 / 40) | |
| 2 | .33 | (.53 / .11 / .06) | .06 | (.06 / .05 / .07) | 33 | (32 / 28 / 56) | ||
| rocq-mcp-evolve | 1 | .48 | (.69 / .28 / .14) | .03 | (.03 / .03 / .04) | 19 | (19 / 17 / 28) | |
| Haiku | 2 | .49 | (.68 / .32 / .14) | .04 | (.04 / .03 / .06) | 20 | (19 / 15 / 43) | |
Table 10: Results on the test split of miniF2F-Rocq for each of the two runs. Same conventions as Table 2 : cost and wall time are computed on the problems solved by all three MCP servers.
| Models | MCP servers | frugal | gauges | ledger | prodauto | triadic | Total |
| control | 4/4 | 3/4 | 3/4 | 0/4 | 0/4 | 10/20 | |
| Sonnet | rocq-mcp | 4/4 | 4/4 | 4/4 | 0/4 | 0/4 | 12/20 |
| rocq-mcp-evolve | 4/4 | 4/4 | 3/4 | 3/4 | 0/4 | 14/20 | |
| control | 0/2 | 1/2 | 2/2 | 0/2 | 0/2 | 3/10 | |
| Opus | rocq-mcp | 2/2 | 2/2 | 2/2 | 0/2 | 0/2 | 6/10 |
| rocq-mcp-evolve | 2/2 | 2/2 | 2/2 | 0/2 | 0/2 | 6/10 |
Table 11: Results on the five project-scale tasks (four runs per task, two for Opus).
| Models | MCP servers | Accuracy | Cost ($) | Wall time (s) |
| control | .50 .12 | 1.56 0.25 | 608 74 | |
| Sonnet | rocq-mcp | .60 .00 | 2.63 1.05 | 595 181 |
| rocq-mcp-evolve | .70 .12 | 1.44 0.84 | 429 202 | |
| control | .30 .14 | 2.19 0.12 | 714 65 | |
| Opus | rocq-mcp | .60 .00 | 2.48 0.27 | 661 142 |
| rocq-mcp-evolve | .60 .00 | 1.89 0.74 | 574 209 |
Table 12: Results on project-scale tasks with standard deviations: across runs for the accuracy (four runs, two for Opus), over the solved runs for the cost and wall time.
| GPT-4o | o4-mini-high | Goedel-Prover-V2 |
| COPRA (GPT-4o) | DeepSeek-Prover-V2 | Ax-Prover (Axiomatic AI) |
| Deepseek R1 | DSP+ | GPT-5 (ReAct, 10 turns) |
| Goedel-Prover-SFT | Bourbaki | TIR Conjecturor |
| ABEL | gemini-2.0-flash-thinking | Enumerate-Conjecture-Prove |
| InternLM2.5-StepProver | gemini-2.5-pro-exp-0325 | Kimina-Prover-7B-Distill |
Table 13: Approaches from the PutnamBench leaderboard used to rank the difficulty of the 60 selected problems. The number of stars indicates the level of performance of the approaches (based on the number of PutnamBench problems each solves).
| MCP servers | Run | Accuracy | Cost ($) | Wall time (s) | |||
| control | 1 | .32 | (.90 / .05 / .00) | .12 | (.10 / .31 / –) | 80 | (73 / 197 / –) |
| 2 | .33 | (.95 / .05 / .00) | .11 | (.11 / – / –) | 75 | (75 / – / –) | |
| lean-lsp-mcp | 1 | .43 | (.95 / .35 / .00) | .14 | (.11 / .60 / –) | 88 | (75 / 298 / –) |
| 2 | .40 | (.95 / .25 / .00) | .11 | (.11 / – / –) | 68 | (68 / – / –) | |
| lean-mcp-evolve | 1 | .35 | (.85 / .20 / .00) | .11 | (.10 / .33 / –) | 62 | (57 / 151 / –) |
| 2 | .33 | (.80 / .20 / .00) | .08 | (.08 / – / –) | 51 | (51 / – / –) | |
Table 14: Results of Sonnet on the 60 problems selected from PutnamBench in Lean for each of the two runs. Same conventions as Table 5 : cost and wall time are averaged over the problems solved by all three MCP servers.