MerLean-Prover：一种用于端到端 Lean 4 定理证明的递归循环框架

MerLean-Prover 是一种端到端 Lean 4 定理证明器，旨在用内核可验证的证明替换“抱歉”声明。该系统由规划、检查和 Lean 三种智能体组成，通过一个递归外环连接，其修订单位为证明计划本身，无需微调、自定义强化学习目标或特定定理的支架。在 FormalQualBench 基准测试中，其表现优于现有最强开源基线；在 Putnam2025 上更是以更低耗时解决全部问题。结果表明，框架设计是与模型能力同等重要的关键因素。