Summary (Overview)

• Evolutionary interface design: The paper proposes a novel evolutionary method where a frontier model (Claude Fable 5) incrementally proposes new features for an agent/prover MCP server, keeping only mutations that measurably improve accuracy, cost, and wall time for smaller models.
• ROCQ-MCP-EVOLVE: The resulting MCP server for the Rocq prover outperforms both a minimal compiler-only baseline (CONTROL) and an established MCP server (ROCQ-MCP) across four models from two families on the miniF2F-Rocq test split.
• Transferability: The evolved toolset ports to Lean (LEAN-MCP-EVOLVE), improving cost and wall time per solve on PutnamBench, though with lower accuracy than the state-of-the-art LEAN-LSP-MCP.
• Key insight: Although only accuracy drove mutation validation, tight time/call budgets led to reduced token usage and tool calls, translating to significant cost and wall time improvements (24% fewer input tokens, 4× fewer output tokens vs. CONTROL).
• Project-scale validation: The evolved server also outperforms baselines on five autoformalization projects requiring multi-file development on top of the MathComp library.

---

Introduction and Theoretical Foundation

The paper addresses a critical bottleneck in AI-assisted theorem proving: the interface between LLM-based agents and proof assistants (Rocq, Lean, Isabelle). While major results are now backed by machine-checked proof certificates, agents interact with proof assistants through interfaces originally designed for human users, not optimized for machine agents. These interfaces are critical because they control:

1. What information the agent receives from the prover
2. The cost of each interaction (tokens, wall time)
3. The capability space of the agent

The theoretical foundation rests on the observation that the set of exposed tools directly influences agents' capabilities at theorem proving. Existing MCP servers (e.g., ROCQ-MCP, LEAN-LSP-MCP) expose tools like search, compile, and interactive debugging, but none have been systematically optimized for agent use. The authors propose treating the interface itself as a design artifact that can be evolved through iterative mutation and selection.

The key insight is that frontier models can serve as orchestrators that propose and implement interface mutations, while smaller models act as testers to evaluate whether each mutation improves measurable objectives. This creates a feedback loop where the interface co-evolves with the agent's needs.

---

Methodology

The Evolutionary Process

The process starts from a CONTROL MCP server exposing only a single tool: compiling an entire file. At each step, an orchestrator (Claude Fable 5) proposes a mutation (new tool, refined output, configuration change). Mutations are evaluated by testers (Claude Haiku 4.5 and Claude Sonnet 5) on curated datasets.

Three tracked metrics:

1. Accuracy: pass@1 proportion of problems solved
2. Cost: average cost in USD per solved problem
3. Wall time: average wall-clock time per solved problem

Phase 1: Mathematical Exercises (6-day deadline)

• Main dataset: dev60 — 60 problems from the Rocq Workbook (20 per difficulty bucket: easy/medium/hard)
• Additional datasets: hard70 (agent collaboration), mathcomp35 (library-specific hints), miniF2F-Rocq valid split (preloading automation)
• Testers: Haiku instances, 2 runs/problem, 300s budget, 30 server calls
• Validation rule: Mutation accepted if net gain ≥ +2 in at least one difficulty bucket without falling below −2 in any other

Phase 2: Project-Scale Tasks ($150 budget)

• Dataset: Five autoformalization projects (tropical algebra, closed real intervals, append-only ledger, finite automata, divisor-sum exercise)
• Testers: Sonnet instances, 4 runs/project, 900s budget, 200 server calls
• Validation: Mutation accepted if >2 additional successes; ±2 threshold corresponds to CONTROL variance

Anti-Cheating System

Ensures correctness by checking that:

• File prefix (imports, statement) is untouched
• No axioms, partial proofs (Axiom, admit, Abort), or additional imports
• Recompilation in a clean directory with Print Assumptions audit

Key Mutations Accepted (chronological)

---

Empirical Validation / Results

miniF2F-Rocq Test Split Results

Table 2 (cost/wall time computed on problems solved by all three servers):

Values in parentheses: easy/medium/hard buckets. Bold = best result.

Key statistical findings:

• ROCQ-MCP-EVOLVE solves more attempts than CONTROL on 91–104 problems, fewer on at most 4 (sign test, p < 10⁻²¹)
• Accuracy gap vs. ROCQ-MCP decreases with stronger models (+15 Haiku, +8 Sonnet, +4 Opus)
• Cost improvements increase with model strength: −45% (Haiku), −54% (Sonnet), −59% (Opus)

Efficiency Results (Table 3, averaged over 4 models)

Project-Scale Tasks (Table 4)

Lean Transfer Results (Table 5, Sonnet on putnam60)

Automation Contribution (RQ3)

auto close alone solved 52/244 problems (21%) on miniF2F-Rocq test split, mostly in the easy bucket (35%). On this subset, cost was $0.03 (vs.$0.06 with ROCQ-MCP) and wall time 11s (vs. 19s). However, automation alone does not explain the full performance gap.

---

Theoretical and Practical Implications

Theoretical Implications

1. Interface as evolutionary artifact: The paper demonstrates that agent/prover interfaces can be systematically optimized through mutation-selection cycles, treating the toolset as a design space rather than a fixed engineering choice.

2. Emergent efficiency from budget constraints: A critical finding is that optimizing only for accuracy under tight budgets implicitly optimizes cost and wall time. The orchestrator discovered that interactive sessions, information-dense error messages, and compact renderings reduce token consumption without explicit optimization pressure.

3. Tool usefulness ≠ tool popularity: The search tool — one of the most popular in existing MCP servers — was heavily used by agents but yielded zero accuracy gain. This challenges assumptions about what tools agents actually need.

4. Model-family independence: The evolved server benefits models from different families (Claude, GPT) and sizes (Haiku → Opus), suggesting the improvements are intrinsic to the interface design, not overfit to specific models.

Practical Implications

1. Cost reduction at scale: With output tokens reduced 4× and input tokens reduced 24%, the evolved server offers substantial cost savings for large-scale proof automation efforts.

2. Project-scale applicability: The tools evolved on standalone exercises transfer to multi-file project development, a critical capability for real-world formal verification.

3. Cross-prover transferability: The core tools are largely prover-agnostic, suggesting the evolutionary method could be applied to other proof assistants (Lean, Isabelle) with similar benefits.

4. Anti-cheating infrastructure: The verification protocol (recompilation, assumption auditing, clean-directory builds) provides a robust framework for trustworthy agent evaluation.

---

Conclusion

The paper presents a successful demonstration of evolutionary interface design for agent/prover interaction. Starting from a minimal compiler-only server, the process grew ROCQ-MCP-EVOLVE, which consistently outperforms both naive and established baselines across:

• Accuracy: +30+ points over CONTROL, +4–15 points over ROCQ-MCP
• Cost: 45–59% reduction vs. CONTROL
• Wall time: 63–64% reduction vs. CONTROL

The method's key innovation is using a frontier model as orchestrator with smaller models as testers, guided by fixed validation rules and anti-cheating protocols. The resulting server is not overspecialized to a model family, transfers to Lean (improving cost/time), and handles project-scale tasks.

Future directions:

1. Run the same evolutionary procedure natively for Lean, allowing the orchestrator to discover Lean-specific features
2. Identify which features of ROCQ-MCP-EVOLVE are intrinsic to agent/prover interaction vs. Rocq-specific
3. The authors note the process is not deterministically replayable but is fully auditable through released logs and mutation tables

The work establishes that interface design is a first-class optimization target for AI-assisted theorem proving, with measurable returns across all key metrics.