在正式数学推理中，设计有效的Lean证明代理是一个核心挑战。除了构建更强大的证明者，最近的研究强调了Lean的工作流程：代理如何分解证明义务、使用工具和编译器反馈、诊断失败、修复证明以及维护结构化证明上下文。受到代码级自我进化代理的启发，我们研究这些工作流程是否可以被进化而非手动设计。
我们提出了一种自我进化的Lean证明代理，其中一个小而固定的可信运行时包裹着一个完全可变的工作空间：证明工作流程、提示和工具。与大多数自我进化系统不同，我们的系统在代理和基准之间进行共演。在每一代中，得分最高的代理（冠军）通过掌握阈值课程更新来修订活动任务分配，只有在当前水平掌握后才会引入更难的证明义务，单一锚定的重新校准会在更新的基准上重新运行冠军，以保持随着难度上升而可比较的分数。
所有进化都保持在Lean基础的验证循环内：无论代理如何自我重写，成功仅在其行为产生Lean验证的证明时才算数，每次尝试必须输出一个机器可读的、Lean基础的证明上下文，其表示形式可能进化但其基础性是被强制执行的。我们运行了共演轨迹和固定基准基线，进行了15代的活跃比较，并在保留的miniF2F测试分割上进行比较。最佳的共演代理达到了45.1%的保留解率，而种子为12.7%，最佳固定基准代理为32.0%。这表明基于验证者的自我进化能够在共演基准下改进Lean证明工作流程。
博主点评： 本文展示了自我进化的Lean证明代理的潜力，尤其是在动态调整证明难度和优化工作流程方面。通过共演机制，代理能够在不断提升的挑战中保持竞争力，推动了形式化证明领域的前沿。