陶哲轩披露 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）的标志性案例。
所属事件:陶哲轩评流体方程爆破新突破，AI 辅助并已 Lean 形式化(9 条相关)→
「漫话AGI」频道最新
- AI 判断哪些职业先被替代：规则能写成代码的那一层先消失 — FinanceYF5 · 2026-10-26
- Anthropic IPO 文件:数年内实现专家级 AI,90% 代码由 Claude 编写 — kimmonismus · 2026-10-26
- 工程师身份危机蔓延:多智能体系统正在重定义软件工程问题 — rakyll · 2026-10-26
- 研究发现：前沿 LLM 常为私利单方面撕毁 AI 合同 — xuanalogue · 2026-10-26
- 133 位专利律师实验：同样用 AI，老手被增强、新人陷入认知卸载 — xiaohu · 2026-10-26
- OpenAI 计算机使用 agent 团队：速度已逼近超越人类专家 — a16z · 2026-10-26