Meta 与 NYU 论文提出 h1 循环，在 PutnamBench 上以更低成本略胜…
New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats hand-built theorem-proving workflows.
Meta 与 NYU 的新论文提出 h1，一个给模型提供快速 Lean 反馈和搜索工具、并在每次校验失败后继续尝试的循环，不预设解题计划，只在每轮开始前生成进度摘要。在相同模型下，h1 在 PutnamBench 上以 598 题对 597 题略胜手工构建的 Goedel-Architect，每题成本为 1.08 美元对 1.47 美元。作者还指出接口仍有影响：使用 Opus 4.8 时，h1 解出 100 道高难度代数题中的 83 道，Claude Code 为 63 道。
推荐理由
AI 评分 60
原文给出同一模型下简单循环与手工工作流的直接对比，以及每道题成本差异，便于判断工作流设计的实际增益。
主题
正文
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.