Meta 与 NYU 论文：简单循环 h1 在 Lean 证明上追平手工工作流
Meta 和 NYU 做了个超简循环 h1，写 Lean 证明不用复杂工作流，成本还比 Goedel-Architect 低三成，代码人可以看看。
Meta 与 NYU 发布论文，提出极简证明循环 h1：只给模型 Lean 快速反馈、搜索工具和每轮开始前的进度摘要，不加入任何人工设计的规划或问题拆分。在同一模型下，h1 在 PutnamBench 的 598 题中以每题 1.08 美元的成本击败 Goedel-Architect 的 597 题与 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.
