Meta与纽约大学的研究人员构建了一个用于证明数学定理的精简人工智能系统，其表现持平甚至超越了精心设计的Lean证明工作流——而且成本更低。

这个名为h1的系统提出一个简单论点：在自动定理证明中，只要模型能获得良好的反馈，简洁可以战胜复杂。

极简智能体循环

这项工作来自Meta的FAIR研究团队和纽约大学。在2026年10月25日发布的论文《h1: A Taste of the Bitter Lesson in Automated Theorem Proving》中，研究人员将h1描述为一个极简的智能体循环，它将前沿大语言模型与Lean 4连接起来，并实时向模型反馈验证器结果。

Lean 4是一个开源证明助手，数学论证以代码形式书写，因此每一步都由编译器而非人工审阅者检查。这种设置让验证器拥有最终决定权：证明只有在通过编译后才算成立。

大多数自动证明器将语言模型包裹在复杂的脚手架中，使用预定义的工作流来拆分问题、分配子任务并协调众多组件。h1框架跳过了这些机制，而是依赖几个简单的机制：

• 持久化文件编辑，模型在一个证明文件上工作，该文件在步骤之间保持状态
• 每次编辑后立即获得编译器反馈，错误即刻显现
• 反思，利用语言模型自身推理问题所在的能力

论文指出，h1的性能主要源于与Lean的高效接口，而非复杂的编排。

基准测试结果

研究报告显示，h1在多个形式化定理证明基准上达到了最先进的水平。在PutnamBench——一个基于William Lowell Putnam数学竞赛（面向北美本科生的年度数学竞赛）题目构建的基准——上，使用GPT-5.5取得了672题中的670分。在FATE-X评估中，h1取得了100分中的90分。

该系统还解决了FormalConjectures集合中的八个未决问题，其中包括以多产数学家Paul Erdős命名的Erdős问题的变体。由于这些问题以Lean的形式语言表述，解决它们意味着产生经机器验证的证明，而非文字论证。

最直接的比较对象是DeepMind的AlphaProof Nexus。在Erdős问题的解决上，h1的成功率为82.5%，而AlphaProof Nexus为76%。成本差距比准确率差距更大：h1每次成功证明花费121美元，而AlphaProof Nexus花费317美元。

苦涩教训在数学中的应用

论文标题指向了"苦涩教训"（bitter lesson）——这一术语由AI研究者Rich Sutton在2019年的一篇文章中提出，指的是依靠大规模计算的可扩展通用方法，长期来看往往胜过专门的手工技术。

这并非Meta在此问题上的首次尝试。该研究建立在Meta早期工作的基础上，包括2022年推出的HTPS神经定理证明器，并反映了方法上的转变。早期系统侧重于围绕模型构建更智能的搜索，而h1侧重于让模型直接与验证器交互。

时机也很重要。h1的结果依赖于GPT-5.5等前沿模型，而其出色的PutnamBench成绩正是使用该模型取得的。

这意味着什么

成本数据是这项工作最具实用价值的部分。每次成功证明的成本从317美元降至121美元，改变的是哪些问题值得尝试。当每次尝试的成本降低时，团队可以对更困难或更具推测性的猜想进行更多次尝试。结果的机器验证特性也是其吸引力的一部分：形式化证明的进展吸引着数学领域之外的广泛关注，因为证明助手也被用于验证软件和硬件设计。

一些注意事项仍然适用。基准分数反映的是在特定测试集上的表现，而PutnamBench在672题中得670分已接近饱和，因此系统在FormalConjectures等未决问题集合上的表现将是接下来最值得关注的衡量指标。h1方法也在很大程度上依赖于其底层的前沿模型。

论文更广泛的信息是：一个强大的基础模型加上干净的验证器反馈，可能比复杂的脚手架更重要——从这些基准来看，这一押注得到了回报。

来源：CryptoBriefing