你请一位数学高手解难题，可以先替他画好路线图：把问题拆成几步，规定先证明哪些引理，再安排不同助手分头处理。也可以只给他一本可查的资料库、一位严格的阅卷员，以及足够多的草稿纸，让他边做边改。自动定理证明长期偏爱前一种办法。h1 这篇论文问的是：如果今天的 AI 已经更会推理，复杂的人工编排还必要吗？
这值得现在看，因为答案可能改变自动定理证明的研发重点。研究团队设计了一个很简单的智能体框架 h1。它不预设如何拆题，也不规定搜索顺序，只让模型使用 Lean 4、读取验证反馈、反思失败原因，然后继续工作。论文报告称，这套简单循环在多项测试中达到当前最佳水平，还解决了 8 个此前被列为开放的问题。不过，所有结果都来自同一研究团队，尚缺独立复核；论文所说的“苦涩教训”，目前更适合作为一项有力主张，而非领域共识。
不教它怎么证明，只让它别停
自动定理证明，是让计算机从公理和已有定理出发，找到一条每一步都符合逻辑规则的证明。它不同于普通数学问答。模型不能只写一段看起来合理的解释，最终答案必须交给程序逐步核验。
这里使用的 Lean 4 是一种证明助手。研究者把命题和推导写成它能检查的严格语言，这叫形式化证明。程序会指出尚未完成的目标和编译错误，也会拒绝用占位符蒙混过关，或偷偷增加原题没有的假设。
h1 围绕这套反馈建立循环。模型在一个持续保留的文件里推理、修改和调用工具；每次编辑后，Lean 立即返回错误与待证目标。模型认为完成后，再把文件交给外部验证器。如果验证失败，另一个语言模型会压缩此前记录，保留已经确认的进展、失败教训和可能有用的引理名称，随后继续下一轮。
关键在于，h1 不替模型安排证明策略。它不要求“先分解，再规划，再调用专门证明器”，只提供搜索数学库、查看定义、测试证明片段等工具。模型自己决定何时查资料、改哪一步、是否换路。
这就是论文标题所说的“苦涩教训”（The Bitter Lesson）：AI 发展中有一条著名经验，长期看，能随着数据和计算扩展的通用方法，往往胜过把大量人类知识手写进系统。h1 把这场争论带到了定理证明。
多给草稿纸，能走多远？
研究团队把“测试时计算”作为主要变量。它指模型回答一道题时投入的计算量，例如搜索更久、修改更多轮。说白了，就是给考生更多草稿纸和思考时间。
在一次运行、没有重复采样或并行尝试的设置下，h1 配合 GPT-5.6 Sol，在 FATE-X 上解出 90/100，在 FormalConjectures100-Solved 上解出 78/100，在 FormalQualBench 上解出 14/23，并完成全部 6 道 IMO 2026 形式化题。配合 GPT-5.5，它解出 PutnamBench 的 670/672。论文把这些结果称为截至 2026 年 8 月 27 日的最佳水平。
有些证明运行得非常久。被接受的单次尝试最多经历 1,123 轮反思压缩、95 个活跃小时，证明文件最长达到 7,124 行。这正是论文想强调的现象：所谓 pass@1——每题只启动一次尝试——不再等于短促的一次作答。只要框架允许，模型可以在同一次运行里放弃旧办法并另寻新路。
在 5 个开放的 Erdős 问题上，h1 使用与 AlphaProof Nexus 相同的 Gemini 3.1 Pro。随着单次尝试预算增加，它达到 82.5% 的成功率，论文按成功条件计算的平均成本为 121 美元；AlphaProof Nexus 的基础版重复三次为 75.4%、191 美元，完整系统为 76%、317 美元。把失败运行也计入后，h1 的单次长尝试达到同样 82.5% 时平均花费 138 美元，而三次重复需要 202 美元。更大预算下，重复尝试仍能取得更高成功率，因此论文并未证明“坚持到底”永远优于“重新开始”。
简单，不等于随便
论文最有价值的修正也在这里：h1 的成绩不能简单归结为“什么都不设计”。框架虽然不规定证明路线，却精心设计了模型与 Lean 的交互方式。
同样使用 Gemini 3 Flash、每题预算 20 美元时，AxProverBase 在 Putnam100 上解出 18 题，h1 解出 69 题。前者每轮反馈后会重新生成完整证明；后者保留工作文件，做局部修改，并立即获得编译反馈。AxProverBase 失败的编译中，有 42.2% 卡在无效的数学库导入，而 h1 预先导入完整 Mathlib，直接消除了这种故障。
工具也很重要。移除搜索、交互式测试环境和语言服务器后，h1 在 Putnam100 与 FATE-X 上分别解出 49 题和 49 题；使用全部工具时升至 69 题和 63 题。论文的消融实验显示，决定效果的不是某一件神奇工具，而是模型能否随时查找、试验，并把反馈用于下一小步。
上下文管理同样影响成本。只在反思之间保留一轮交互时，h1 解出 50 道 Putnam100 和 39 道 FATE-X；保留十轮时增至 72 和 65。可若拉长到 200 轮，成绩又降到 60 和 52。长上下文虽然能利用缓存、降低重复读取成本，却也可能逐渐变得混乱。h1 的做法是在保留进展与及时压缩之间取平衡。
为什么值得关注
这项工作挑战的不是某一种证明技巧，而是一套评价习惯。过去，不同系统都可能把一次运行称为 pass@1，但一次可能允许 16 次计划修订，另一次允许 50 轮智能体操作。只比较“尝试次数”，并不能说明谁更高效。h1 因而主张同时控制模型，并比较实际推理成本。
如果结果能够独立复现，它传递的信号很清楚：在为 AI 手工设计复杂证明流程前，应先测试一个工具可靠、反馈及时、能持续工作的简单循环。人类的设计重点也许会从“替模型规定怎么想”，转向“让模型更顺畅地试、查、改和验证”。
局限与未知
- 论文主要使用闭源前沿模型，无法完全判断训练数据是否包含部分题目或相关解法。研究者在可能时选用了早于题目发布的模型，但不能彻底排除数据暴露。
- h1 目前主要处理单个 Lean 文件。跨多个文件的大型形式化工程还需要依赖管理、代码库级验证和多智能体协作，论文没有证明简单循环在这种规模下仍占优势。
- 8 个开放问题的“已解决”来自 Lean 对形式化命题的验证。形式证明通过，不自动保证形式化命题准确表达了原始数学问题；论文自己也发现过缺少假设的错误形式化。其开放性判定与数学意义仍需要独立专家审查。