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

Meta FAIR 联合 EPFL、NYU 等机构发布论文 h1，提出让单一模型在纯 Lean 反馈循环中反复尝试长序列证明、不再依赖手工设计的系统编排，从而在形式化定理证明上刷新 SOTA。Richard Sutton 转发称这是「苦涩教训」的又一例证：算力驱动的通用方法胜过精心的人工设计。