Evolving a proof-assistant interface improves agents' Rocq theorem solving

An AI agent writing a formal proof depends on more than its model weights. The interface determines whether it repeatedly compiles entire files, inspects a live proof state, or receives useful feedback after a failed tactic. Growing an Agent/Prover Interface investigates whether those tools can be improved through measured, incremental changes.
The researchers introduce rocq-mcp-evolve, an MCP server for the Rocq proof assistant. A frontier model proposes mutations to the interface, while smaller models test whether each change improves theorem solving. The process retains useful changes and rejects those that do not meet its validation rules.

Changing the tools, not the tested models

The experiment starts with a server exposing a single operation: compiling a whole file. Mutations can add a tool, change its output, or adjust configuration. Evaluation first uses mathematical exercises and then five project-scale tasks.
The authors use Claude Fable 5 as the orchestrator and Haiku 4.5 and Sonnet 5 as testers. Humans set the environment, budgets, and validation rules and conduct a daily review, rather than manually designing each mutation.
More tools did not automatically improve performance. A search tool for applicable lemmas was rejected after agents used it heavily without gaining accuracy. A proposed team of three agents was also rejected. These examples make the selection process important: the final interface is not simply an accumulation of plausible features.

Interactive sessions reduce repeated work

The final server maintains a live session containing the current proof state. Agents can apply tactics, backtrack, and inspect that state without reconstructing it through full compilation on every interaction. The interface also exposes automation and verification tools.
Proof checking includes defenses against shortcuts that would invalidate the experiment. The harness protects the original statement and imports, rejects partial proofs and added axioms, recompiles in a clean directory, and audits theorem assumptions. Project checks also build the submitted files and run their test suite.
Those checks distinguish a successfully verified proof from an agent merely reporting success. They remain part of the workflow rather than being replaced by the model's confidence.

Held-out results and their limits

On the disjoint test split of miniF2F-Rocq, the researchers compare the evolved server with a compiler-only control and the established rocq-mcp interface across four models. For example, Haiku's reported accuracy rises from 17% with the control and 33% with rocq-mcp to 48% with the evolved server. Sonnet reaches 80%, compared with 50% and 72%.
The principal cost and wall-time comparisons use a shared subset of problems solved by all three servers in at least one run. They should not be interpreted as unrestricted savings on every attempted theorem.
The Lean transfer also has a qualification: the paper reports lower overall solve rate than lean-lsp-mcp, despite improvements in cost and time per solve. Project-scale tasks were used during evolution, although no mutations from that phase were accepted. The strongest conclusion is that interface design can materially affect these evaluated agents, not that one toolset is optimal for every prover or workload.