OpenAI 宣称攻克纳维-斯托克斯问题，Lean 形式化证明已开源

AlexKontorovich · x · 2026-09-09

数学界权威机构与 Lean 社区对 OpenAI 宣称在纳维-斯托克斯问题上的突破作出回应。AMS 会长 Ravi Vakil 与 CEO John Meier 发声明称，这一进展是「人类知识的一个里程碑式突破」，并梳理了脉络：从 Navier、Stokes、Leray、Ladyzhenskaya 的经典工作，到 Córdoba 与 Martínez-Zoroa 的近期突破，再到 Alpöge 与 Buckmaster 借助新技术推进，最后由 OpenAI 数学家完成关键步骤。

Lean 社区表示对此消息「和所有人一样完全意外」，并放出了两条可查阅的 Lean 形式化证明：Alpöge/Buckmaster 版本与 OpenAI 版本。Tristan Buckmaster 的 fluidlean 仓库（含 affinecore、boussinesq-blowup、euler-blowup 等目录）已公开，目前 143 stars、11 forks。