Meta 与 NYU 论文提出简化数学证明流程 h1

Meta 和纽约大学的一篇新论文表明，一个配备好用的 Lean 工具和更多算力的简单循环，能够达到或超越人工构建的定理证明工作流程。

用 Lean（一种可供计算机检查的语言）编写数学证明的系统，越来越多地采用人工设计的工作流程来规划和拆分问题。这些系统的性能提升往往伴随着更强的模型或更多算力，因此难以看清工作流程本身带来了什么。

他们构建了 h1：一个为模型提供快速的 Lean 反馈和搜索工具，并让模型在每次检查失败后继续工作的循环。它不规定计划，只要求在每一轮开始前提供进展摘要。

在使用相同模型的情况下，h1 在 PutnamBench 上以解决 598 道题对 597 道题的成绩胜过人工构建的 Goedel-Architect，平均每题成本为 1.08 美元，对方为 1.47 美元。接口仍然重要：使用 Opus 4.8 时，h1 解出了 100 道高难度代数题中的 83 道，Claude Code 则解出了 63 道。