The authors began with a minimal Model Context Protocol (MCP) server exposing only the Rocq compiler.
Evolved prover interfaces make theorem-solving agents faster and cheaper
A model-designed MCP server improved proof success, cost, and runtime across Rocq agents, with efficiency gains transferring to Lean.
Research Lab
Jules Viennot · Guillaume Baudart · Marc Lelarge
IRIF · Université Paris Cité · Inria · CNRS · DI ENS
Research Digest··2 min read
Thread:Agent Harness Optimization
Viennot, Baudart, and Lelarge treat the interface between an AI agent and a proof assistant as an optimization target.
Why this paper
From Inria and 5 others · Released code · Part of Agent Harness Optimization, now 82 papers
In one line
An evolutionary method designs MCP servers for proof assistants, improving cost and solve rate.
What it released
Code
What we could check
- ✓Code link in the paper (github.com)
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ✓Limitations stated by the authors
- ·No benchmark numbers found
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§