Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
cs.AI
Submitted: 2026-09-30
Updated: 2026-10-08
Code: https://github.com/LLM4Rocq/rocq-mcp-evolve-experiment
Sources
- Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
- A complete formalization of Fermat's Last Theorem for regular primes in Lean
- Large Language Models as Tool Makers
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
- Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
- Is Bash All You Need? An Empirical Study of Tool Interfaces for Enterprise Digital Worker Agents
- Alita-G: Self-Evolving Generative Agent for Agent Generation
- A Self-Improving Coding Agent
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
- MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
- Voyager: An Open-Ended Embodied Agent with Large Language Models
- AI-Assisted Completion of CertiGC Proofs: An Experience Report
- TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Tasks
- The Devil Is in the Interface: Evaluating How Tool Architecture Shapes Coding Agent Behavior
- SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering
Related papers
- MAVEN-T: Reinforced Heterogeneous Distillation for Real-Time Multi-Agent Trajectory Prediction
- Model Discovery Agent: LLM-assisted Bayesian experiment design for data-efficient discovery of mechanistic world models
- Agents' Last Exam
- The Clinician's Veto: Navigating Trust, Liability, and Uncertainty in Autonomous AI Prescribing
- MindHelper: Closed-Loop Embodied Mental-State Reasoning for Precision Intervention
- Incumbent Advantage: Brand Bias and Cognitive Manipulation Dynamics in LLM Recommendation Systems