Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

Research Approach

This paper investigates whether Lean theorem-proving agents can autonomously improve their proof workflows—such as proof decomposition, tool usage, and error diagnosis—rather than relying on hand-designed strategies. The authors introduce a self-evolving system where a trusted, fixed runtime wraps a fully mutable workspace. The agent is permitted to rewrite its own prompts, tools, and workflows, provided that all proof attempts are verified by the Lean compiler. A key innovation is the coevolution of the benchmark: as the agent masters easier tasks, the system automatically replaces them with harder problems from a stratified pool, using a single-anchor recalibration method to ensure performance remains comparable across generations.

Key Findings

The researchers compared their coevolving agent against a fixed-benchmark baseline over 15 generations. While the fixed-benchmark agent reached a 32.0% solve rate on a held-out miniF2F test split, the coevolving agent achieved a 45.1% solve rate. The results demonstrate that allowing the benchmark to harden alongside the agent provides a more effective evolutionary signal, preventing the saturation that often occurs when agents are evaluated against static, easier problem sets. The study also highlights that the agent successfully evolved its own proof-context representations, which remained grounded in Lean verification despite the agent's ability to modify its internal logic.

Formal theorem proving is often bottlenecked by the rigidity of human-designed proof workflows. By demonstrating that agents can evolve their own workflows while maintaining rigorous, verifier-grounded correctness, this work suggests a path toward more autonomous and scalable mathematical reasoning systems. The coevolutionary framework provides a template for training agents in environments where the difficulty of the task must adapt to the agent's growing capabilities, a critical requirement for open-ended problem solving.