用递归循环框架自动补全Lean4定理证明，无需微调或定制奖励。
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
- 三类智能体协作，以证明计划为单位递归优化。
- 在23个博士资格考题中解决10题，超越现有开源基线。
- 适配小模型，可让Sonnet完全解决4道题，适合研究自动化证明者。
MerLean-Prover 是一个端到端的 Lean4 定理证明系统，将 'sorry' 声明替换为内核可验证的证明。它由三种智能体（规划、检查、Lean）组成，通过递归外层循环迭代更新证明计划，无需微调、无自定义强化学习目标，也无定理特定的辅助结构。在包含23个博士资格考试定理的 FormalQualBench 上，该系统解决10/23题，超过最强公开基线 OpenGauss（8/23）。在 Putnam2025 挑战中，同一框架成功完成全部12题，且总运行时间远低于次优系统。该框架还具备迁移能力：Sonnet 能完整解决4个测试问题，Haiku 解决其中两个短题。结果表明，证明框架设计是端到端 Lean4 证明的关键因素，与模型能力同等重要，且简单框架已具高效性。
原文摘要 · Abstract (English)
MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。