Meta 与 NYU 论文：简单循环 h1 打平手工定理证明工作流
rohanpaul_ai · x · 2026-11-02
Meta 与 NYU 的论文《h1: A Taste of the Bitter Lesson in Automated Theorem Proving》提出一个极简 agent 循环 h1：只给模型高效的 Lean 4 接口，靠验证器反馈和自我反思持续迭代，不强加规划或分解结构。
- 在 PutnamBench 上，同模型条件下 h1 以 598:597 击败手工工作流 Goedel-Architect，且单题成本 $1.08 对 $1.47
- 用 Opus 4.8 时，h1 在 100 道高难代数题上解出 83 道，Claude Code 仅 63 道
- 结论呼应「苦涩的教训」：收益主要来自简单循环+更多算力，而非精巧的手工工作流；高效的 Lean 接口才是决定成本与解题率的关键
所属事件:Meta 与 NYU 极简循环 h1 刷新定理证明纪录(2 条相关)→
「编程与Agent」频道最新
- Stardock 创始人用 AI 让游戏角色免 rigging 直接眨眼说话 — draginol · 2026-11-02
- 101 个 agent 干一个工作室的活:Stardock 创始人晒 AI 编队实操 — draginol · 2026-11-02
- Google 开源内部千名工程师在用的「大象-金鱼」AI 编码插件 — solyarisoftware · 2026-11-02
- DeepSeek SuperAgent 架构遭质疑：多 Worker 共享事件流恐引发冲突 — teortaxesTex · 2026-11-02
- 开发者把手表改成语音入口:按住录音,Grok Bot 自动分派任务 — johnlindquist · 2026-11-02
- Matt Pocock:让状态只存一处,Redux 思路或成 Agent 工程解药 — mattpocockuk · 2026-11-02