陶哲轩转发流体方程奇点突破:论证已用 Lean 形式化,逼近 Navier-Stokes

MannyKayy · x · 2026-09-08

Terence Tao 在博客介绍 Alpöge 与 Buckmaster 基于 Córdoba 与 Martínez-Zoroa 工作的新突破:在三个更简单的模型方程(不可压多孔介质方程、二维 Boussinesq 方程、三维不可压 Euler 方程)上构造出光滑初始条件与光滑外力项下的有限时间奇点(爆解)。这一方法很可能同样适用于 Navier-Stokes 方程——即千禧年大奖难题的全正则性问题,业界普遍预期「光滑数据+光滑外力导致有限时间爆解」 soon 可被完全证明。值得一提的是,该论证已借助现代 autoformalization agent 在 Lean 中完成形式化。博主评论认为,陶哲轩对 AI 的积极立场显著影响了数学界对 AI 的接受度——多数数学家原本并不把 AI 领域当回事。