新的 Meta 与 NYU 论文表明：一个搭配优质 Lean 工具和更多算力的简单循环，足以媲美甚至超越人工设计的定理证明工作流。
研究者构建了 h1：一个给模型提供快速 Lean 反馈和搜索工具的循环，验证失败后仍继续推进，每轮之前只给出一份进度摘要、不预设计划。在同一模型下，h1 在 PutnamBench 上以 598 对 597 击败人工设计的 Goedel-Architect，单题成本为 1.08 美元对 1.47 美元；搭配 Opus 4.8 时，它在 100 道高难度代数题中解出 83 道，而 Claude Code 为 63 道。这很重要，因为它表明对自动定理证明而言，好的工具与反馈可能比精巧的人工工作流更关键。
报道来源
- Rohan Paul2026-11-01 19:25