原帖引用 · AI 翻译
标题：“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 道。
原文
New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats hand-built theorem-proving workflows. Systems that write math proofs in Lean, a language a computer can check, increasingly use hand-designed workflows that plan and split up problems. Their gains often come with stronger models or more compute, hiding what the workflow adds. They built h1, a loop that gives the model fast Lean feedback and search tools, and keeps it working after each failed check. It imposes no plan, only a progress summary before each new round. With the same model, h1 beat the hand-built Goedel-Architect on PutnamBench, 598 problems to 597, at $1.08 against $1.47 per problem. The interface still matters: with Opus 4.8, h1 solved 83 of 100 hard algebra problems, against 63 for Claude Code.