陶哲轩评流体方程爆破新突破，AI 辅助并已 Lean 形式化
陶哲轩在博客撰文介绍数学家 Levent Alpöge 与 Tristan Buckmaster 在流体方程正则性方向的最新突破，称其为「a remarkable achievement」（一项了不起的成就），并指出论证包含大量 AI 输入，相关工作已在定理证明器 Lean 中形式化。该方向关联千禧年大奖难题之一——三维不可压 Navier-Stokes 方程整体正则性问题（奖金 100 万美元）。
已确认
- Alpöge 与 Buckmaster 在 Córdoba 与 Martínez-Zoroa 工作基础上改进方法，已在三个更简单的模型方程上证明有限时间爆破：不可压多孔介质方程、二维 Boussinesq 方程、三维不可压 Euler 方程（据 @peterjliu、@MannyKayy 转述陶哲轩博客）。
- 陶哲轩评价这一成果为「a remarkable achievement」，并提及论证包含大量 AI 输入，作者们近期在该方向连续推进（@Hesamation）。
- 论证已用 Lean 形式化（@peterjliu、@MannyKayy）。
- @basedjensen 汇总称该领域正「异常快速」推进：除 Alpöge/Buckmaster 的光滑强迫项（smooth-forced）Euler 结果外，另一团队独立提出了非强迫（unforced）情形的相关结果；陶哲轩认为完整的光滑解证明或已可行。
- @alexisgallagher 转述称，学界目前普遍预期可以构造出相关光滑初始条件下的爆破解，进一步逼近完整 Navier-Stokes 问题。
- 多条转述帖（@burnytech、@LucaAmb、@Singularitarian）指出陶哲轩认为该爆破机制或可延伸至 Navier-Stokes 方程本身；其中 @Singularitarian 的转述还提及 OpenAI 与该工作的关联，但细节未在材料中展开。
尚未确认
- 完整的三维不可压 Navier-Stokes 方程爆破/正则性结果尚未证明，目前的结论限于模型方程与 smooth-forced 情形。
- @Singularitarian 提到的 OpenAI 关联缺乏细节，无法核实具体合作形式。
为什么重要
- 这一进展沿「先在更简单模型方程上证明爆破、再逼近完整 Navier-Stokes」的路线推进，是千禧难题研究路径上的实质进展。
- AI 在数学研究中的深度参与（陶哲轩特别指出论证含大量 AI 输入）以及 Lean 形式化带来的可验证性，展示了人机协作证明前沿数学的新范式。
2026-09-08 ~ 2026-09-10 · 9 条相关
一手来源
- Terence Tao 评价 AI 参与的数学新突破：方法有望延伸至 Navier-Stokes — Hesamation ·
- 陶哲轩披露 Navier-Stokes 突破:三种方程有限时间爆破已证,且已用 Lean 形式化 — peterjliu ·
- 陶哲轩确认Navier-Stokes爆破证明临近,AI辅助工作已用Lean形式化 — littmath ·
- 【源头】陶哲轩披露 Navier-Stokes 突破:三种方程有限时间爆破已证,且已用 Lean 形式化 — peterjliu · 2026-09-08
- 流体正则性问题进展神速:Tao 称光滑解证明或已可行 — basedjensen · 2026-09-08
- Terry Tao 撰文评 Buckmaster 团队构造流体方程爆破解 — LucaAmb · 2026-09-08
- 【源头】Terence Tao 评价 AI 参与的数学新突破：方法有望延伸至 Navier-Stokes — Hesamation · 2026-09-08
- Alpöge 与 Buckmaster 发布新反例结果，陶哲轩称其机制或可延伸至 Navier-Stokes — burny_tech · 2026-09-08
另有 4 条近重复转述:Singularitarian · MannyKayy · littmath · alexisgallagher