The authors began with a minimal server exposing only the Rocq compiler.
Evolved prover interfaces make AI theorem proving cheaper and faster
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··3 min read
Viennot, Baudart, and Lelarge treat the interface between an AI agent and a proof assistant as an object to optimize rather than fixed infrastructure.
Why this paper
From Inria and 5 others · Released code
In one line
Evolutionary design of MCP tools for proof assistants, keeping only features that improve smaller models, yields better success rate, cost, and time.
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
- ·No stated limitations found
- ·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.
§