h1：自动定理证明中的苦涩教训

简单代理循环加高效 Lean 接口可匹配专用定理证明工作流。

资讯摘要

论文提出 h1，一个简单代理循环框架，为模型提供高效的 Lean 4 接口，依靠验证器反馈与自我反思持续工作，不预设分解或搜索结构。作者报告 h1 在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上取得当前最佳结果，并解决 FormalConjectures 中八个开放问题；在相同模型下，其表现匹配或超过 Goedel-Architect、AlphaProof Nexus 等专用工作流。消融与对比显示，高效的 Lean 接口在很大程度上决定成本与求解率。

要点速读

1. h1 不施加分解或搜索结构，仅通过 Lean 4 接口与验证器反馈驱动模型迭代。
2. 作者报告其在 PutnamBench、FATE-X、FormalConjectures100-Solved 上达到当前最佳，并解决八个开放问题。
3. 与 Claude Code、AxProverBase 的匹配模型对比表明，高效 Lean 接口是成本与求解率的主要因素。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/29 08:00:20（北京时间）。