{"id":"arxiv/2607.17352","url":"https://arxiv.org/abs/2607.17352","tags":["cs.AI","cs.LG","quant-ph"],"score":0,"title":"Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution","domain":"cs.AI","source":"arxiv","authors":["Yuqing Li","Zeguan Wu","Yu Gan","Junyu Liu"],"reviews":0,"subject":"cs.AI","summary":"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,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-19","reactions":{}}