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

Yuqing Li, Zeguan Wu, Yu Gan +1

Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: ho…