Meta FAIR 发布 h1，纯 Lean 反馈循环刷新定理证明 SOTA

Meta FAIR 联合 EPFL、NYU 等机构发布论文《h1: A Taste of the Bitter Lesson in Automated Theorem Proving》。其核心思路是不再依赖手工设计的系统编排，而是让单一模型在纯 Lean 反馈循环中反复尝试长序列证明，最终在形式化定理证明上取得 SOTA。Richard Sutton 转发并称其为「苦涩教训」的又一例证：算力驱动的通用方法胜过精心的人工设计。

2026-10-13 ~ 2026-10-13 · 2 条相关