OpenAI 与 Alpöge-Buckmaster 攻克 Navier-Stokes 都重度依赖 Lean 形式化验证
fortnow · x · 2026-09-10
Lance Fortnow 撰文指出,OpenAI 与 Tristan Buckmaster/Levent Alpöge 两组关于 Navier-Stokes(千禧年难题)的宣布都重度依赖 Lean 证明助手:OpenAI 将结果完整在 Lean 中形式化;Buckmaster 团队公开的三个结果已通过 Lean 验证,但「hypo-dissipative Navier-Stokes 的 blowup」结果因 Lean 验证未完成而暂缓公布。文章回顾了 Leonardo de Moura 2013 年在微软启动的 Lean 项目及其演进(包括缺乏向后兼容导致的库维护困境),以及 Hales 的 Kepler 猜想、Scholze 的 liquid tensor experiment 等大型 Lean 形式化项目。他发问:Lean 是否正成为数学发表的新门槛?
所属事件:OpenAI 宣称攻克 Navier-Stokes，另一千禧难题亦有进展(21 条相关)→
「漫话AGI」频道最新
- a16z：改变世界的技术都先「混乱入场」，Agent 正走同样的路 — a16z · 2026-10-27
- 给 AI 末日定概率的人：Lifland 称不减速则接管概率约 67% — NathanpmYoung · 2026-10-27
- 程序员警告:模型「消融版」将冲击软件供应链,千级依赖无人设防 — nitarshan · 2026-10-27
- 程序员观点：每次 SOTA 模型发布，都该主动「删掉」部分旧认知 — zack_overflow · 2026-10-27
- Replit 预言：2030 年前每家财富 500 强都将是「自驾公司」 — amasad · 2026-10-27
- Anthropic 称全保险业也兜不住自身风险，网友嘲讽 — GarrisonLovely · 2026-10-27