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

arXiv: https://arxiv.org/abs/2607.17352 · HTML: https://mlsanity.com/paper/2607.17352/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 31 of its 38 references that are in the map.
- First posted on arXiv 19 Jul 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 31)

- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [Promptbreeder: Self-Referential Self-Improvement Via Prompt Evolution](https://mlsanity.com/paper/2309.16797/) (2023)
- [AFlow: Automating Agentic Workflow Generation](https://mlsanity.com/paper/2410.10762/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Automated Design of Agentic Systems](https://mlsanity.com/paper/2408.08435/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Darwin Godel Machine: Open-Ended Evolution of Self-Improving Agents](https://mlsanity.com/paper/2505.22954/) (2025)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Emergent Complexity and Zero-shot Transfer via Unsupervised Environment Design](https://mlsanity.com/paper/2012.02096/) (2020)
- [AutoAgents: A Framework for Automatic Agent Generation](https://mlsanity.com/paper/2309.17288/) (2023)
- [Paired Open-Ended Trailblazer (POET): Endlessly Generating Increasingly Complex and Diverse Learning Environments and Their Solutions](https://mlsanity.com/paper/1901.01753/) (2019)
- [A Survey of Self-Evolving Agents: What, When, How, and Where to Evolve on the Path to Artificial Super Intelligence](https://mlsanity.com/paper/2507.21046/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [AgentSquare: Automatic LLM Agent Search in Modular Design Space](https://mlsanity.com/paper/2410.06153/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Automatic Curriculum Learning For Deep RL: A Short Survey](https://mlsanity.com/paper/2003.04664/) (2020)
- [Self-Taught Optimizer (STOP): Recursively Self-Improving Code Generation](https://mlsanity.com/paper/2310.02304/) (2023)
- [EvoAgent: Towards Automatic Multi-Agent Generation via Evolutionary Algorithms](https://mlsanity.com/paper/2406.14228/) (2024)
- [A Survey on Self-Evolution of Large Language Models](https://mlsanity.com/paper/2404.14387/) (2024)
- [A Self-Improving Coding Agent](https://mlsanity.com/paper/2504.15228/) (2025)
- [Multi-Agent Evolve: LLM Self-Improve through Co-evolution](https://mlsanity.com/paper/2510.23595/) (2025)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Hyperagents](https://mlsanity.com/paper/2603.19461/) (2026)
- [GenEnv: Difficulty-Aligned Co-Evolution Between LLM Agents and Environment Simulators](https://mlsanity.com/paper/2512.19682/) (2025)
- [The Red Queen G"odel Machine: Co-Evolving Agents and Their Evaluators](https://mlsanity.com/paper/2606.26294/) (2026)
- [LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks](https://mlsanity.com/paper/2606.03303/) (2026)
- [DeepFact: Co-Evolving Benchmarks and Agents for Deep Research Factuality](https://mlsanity.com/paper/2603.05912/) (2026)
- [Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement](https://mlsanity.com/paper/2606.06468/) (2026)

## Built on by (most cited first, 1 of 1)

- [Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean](https://mlsanity.com/paper/2609.39544/) (2026)

## Abstract (arXiv)

Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.