陶哲轩披露 Navier-Stokes 突破:三种方程有限时间爆破已证,且已用 Lean 形式化
peterjliu · x · 2026-09-08
陶哲轩在博客撰文介绍 Alpöge 与 Buckmaster 基于 Córdoba 与 Martínez-Zoroa 工作的新进展，方向是千禧年大奖难题之一——三维不可压 Navier-Stokes 方程的整体正则性问题，奖金 100 万美元。
- 学界现在普遍预期：可以构造光滑初值与光滑外力项使方程在有限时间产生奇点，甚至不需要外力项也能做到
- 两位作者尚未完全达成目标，但突破已足以让完成目标「近期非常可行」
- 他们已在三个更简单的模型方程上证明了有限时间爆破：不可压多孔介质（IPM）方程、二维 Boussinesq 方程、三维不可压 Euler 方程
- 所用方法很可能同样可推广到 Navier-Stokes
- 论证已在 Lean 中完成形式化——这借助了当下自动形式化 agent 的能力
如果完整证明落地，将是数学史级成果，也是 AI 辅助数学研究（autoformalization agents）的标志性案例。
「漫话AGI」频道最新
- 软件开发已率先变身「机器人管理」，其他工作会跟上吗 — StrategicHarmony · 2026-09-08
- bantel 犀利发声:拒绝用 AI 反编译省下数万小时,是表演式的残忍 — banteg · 2026-09-08
- tinyfool 谈能耗之争:碳基演化数亿年,硅基才百年 — tinyfool · 2026-09-08
- 复旦联合斯坦福牛津等 12 机构发布 68 页 AI 生产力综述 — jiqizhixin · 2026-09-08
- OpenAI 研究员谈纳维-斯托克斯风波:数学是全人类的团队运动 — jachiam0 · 2026-09-08
- 传耶鲁经济学家发文论证 AGI 将掏空经济中所有「配件型工作」 — mikeflache · 2026-09-08