Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu
cs.AI, cs.LG, quant-ph
2026-07-20
A small trusted runtime wraps a fully mutable workspace and coevolves the agent with its benchmark, with each generation's champion rewriting the task distribution. After 15 generations the held-out miniF2F solve rate rises from 12.7% for the seed to 45.1%, versus 32.0% for a fixed-benchmark baseline.
In formal mathematical proof with Lean, an agent's strength depends not only on the prover but on the workflow around Lean: how it decomposes proof obligations, uses tools, reads compiler feedback, diagnoses failures, repairs proofs, and maintains proof context. Hand-designed workflows (LEAP, Goedel-Architect) push miniF2F-test to 99.2%, showing that workflow is a major performance determinant. The paper asks: can such workflows be evolved instead of hand-designed?
The architecture is a small, fixed, trusted runtime wrapping a fully mutable workspace. The runtime handles correctness (Lean verification, evaluation, benchmark management) and stays out of the evolutionary search; the proof workflow, prompts, and tools inside the workspace are all mutable and free for the agent to rewrite.
Unlike most self-evolving systems, this one coevolves the agent with its benchmark. Between generations, the highest-scoring agent (the champion) revises the task distribution in two ways. First, a mastery-throttled curriculum introduces harder problems only after the current level is mastered: when a level's mastery m falls below the threshold 0.70 it gets lateral replacement, and at 0.70 it graduates to the next level. Second, single-anchor recalibration reruns the champion on the updated benchmark to keep scores comparable after changes.
All evolution stays inside a Lean-grounded verification loop. However the agent rewrites itself, a success counts only when its behavior yields a verified proof under a trusted Lean snapshot; every attempt must emit a machine-readable, Lean-grounded proof context, whose representation may evolve but whose groundedness is enforced. This re-verification is built to prevent spoofing: it rejects top-level Lean commands, requires real proofs, and sanitizes certificates.
The system runs for 15 active generations with a 76-task active benchmark (initial L1:L2:L3 = 27:46:3), evaluated on a held-out miniF2F test split (244 problems) never used in training, using a DeepSeek backend (deepseek-v4-pro, greedy decoding):
| Configuration | Held-out solve rate |
| Seed agent | 12.7% |
| Best fixed-benchmark agent | 32.0% |
| Best coevolving agent (Gen 15) | 45.1% |
The benchmark difficulty coefficient rises from 1.00 to 3.17, showing the curriculum is getting harder. Coevolution beats the fixed benchmark by 13 points, validating the value of growing agent and benchmark together.
A counterintuitive finding from the evolution: the winning workflow is repair-centered (generate a proof, read Lean feedback, bounded retry), not decomposition-centered. Decomposition workflows keep appearing but get competed away, because each extra decomposition step adds failure points (JSON parse errors, non-self-contained lemmas, longer prompts, timeouts). The evolved mutable tools mostly check hallucinated Lean names (#check probes, lemma verification, namespace-aware search). Very large repair loops (10-12 attempts) also get competed away for instability.
For anyone working on formal proof or agent workflows, this demonstrates a low-labor route: skip hand-designing the workflow and let it grow inside a trusted verification loop. More importantly, it turns the benchmark from a passive ruler into an active coevolving partner, using a mastery-throttled curriculum to auto-tune difficulty and avoid the problem where a fixed benchmark gets saturated early and loses training signal. The idea is not specific to Lean; any agent setting with a trusted verifier can borrow it.
The held-out 45.1% is still far from the 99.2% of hand-designed Goedel-Architect (though backends differ, so not strictly comparable), suggesting that evolution to top hand-designed workflows needs more distance, possibly longer runs or larger populations. The study is a single run with no variance estimate. The winning route stays repair-centered; decomposition never took hold, and the authors themselves think verified decomposition should be rewarded directly. Proof contexts stabilize as shallow supports rather than deep dependency graphs. The backend shows non-negligible output instability even at temperature 0.