人类数学家的反击：N-S方程证明正确性存疑
中科院物理所 · 科学与科普
李璐 2026-11-07 12:26 北京 以下文章来源于：赛先生 赛先生 导读： OpenAI宣称解决纳维-斯托克斯方程（Navier-Stokes equations，简称N-S方 导读： OpenAI 宣称解决纳维 - 斯托克斯方程 （ Navier-Stokes equations ，简称 N-S 方程） 问题近两个月后，数学界仍未就 OpenAI 是否真正解决这一问题达成共识。截至 11 月 2 日， N-S 方程问题在克雷研究所官网上尚未被列为“已解决问题”。 10 月 6 日，伦敦国王学院应用数学讲师亚历山大·巴斯图尼斯 （ Ale xander Bastounis ） 、剑桥大学博士法比安·奇尔切利 （ Fabian Circelli ） 和安德斯·汉森 （ Anders C. Hansen ） 在 arXiv 网站上发布论文，指出对于 N-S 方程的证明， OpenAI 公开的自然语言证明与 Lean 形式化证明存在不一致。 这意味着， OpenAI 公布的计算机验证结果，并不能直接证明其面向人类读者的数学论文正确。 论文《 Navier – Stokes lost in translation 》图源：参考文献 [1] 此前， OpenAI 还被质疑或使用了未公开的人类数学家研究思路以及数据，并在研究尚未充分核查的情况下抢先发布了一份仓促的证明。《赛先生》曾梳理过相关人类数学家与 AI 公司的互动过程。 此次，人类数学家对 OpenAI 发布的该证明的正确性提出质疑。 SAIXIANSHENG Lean形式化与论文中的证明存在差异 9 月 8 日， OpenAI 以公司独立署名发布了一份 N-S 方程 存在性与光滑性问题的证明， 同时 公开了 Lean 形式化代码。 前者使用传统的数学语言与符号编写，是供人类阅读的自然语言版本，后者则借助 Lean 语言，将复杂定理完全形式化，以使用计算机验证数学证明中每一步推理的正确性。 但通过了 Lean 形式化验证，只能说明用 Lean 语言书写的证明逻辑推导无误，并不等于自然语言的证明正确。因为 计算机验证发挥作用的前提是，该自然语言证明被正确转化为形式化语言。 如果翻译过程中改变了数学条件或结论，计算机验证的就可能不再是原来的命题。 此次数学家质疑的，就是 OpenAI 的自然语言证明并没有被准确转化为 Lean 语言。 研究人员 发现， OpenAI 的两个版本证明 至少存在两处不一致 。 第一处是 证明中 的引理 8.6 ：为保证解光滑到 m 阶， 在自然语言证明中， 要求函数光滑到 m+4 阶导数 。 但 在 Lean 形式化 中，对应的值 为 m+5 阶。 m+ 5 是更宽松的条件 ，在 数学 条件 上更弱。 第二处是引理 10.5 ：相对于自然语言版本， Lean 形式化版本中公式的上界依赖新增了梯度项 A R 。 研究人员认为，这些差异意味着， Lean 形式化并没有逐项准确验证自然语言论文的全部证明，而是验证了更宽松条件下的数学命题 。 此前， OpenAI 发布的信息显示，其模型 GPT-6 Astra 耗时 17 小时，将证明形式化为 Lean 代码并验证。 提出质疑的三位作者之一奇尔切利 表示 ， “ 我们的论文利用可解性复杂 度 指数 （ SCI ） 层级和逻辑工具 ，揭示了 AI 在 形式化 工作中的局限性 。 ” 需要指出的是， 研究人员 并没有因此 证明 OpenAI 的 自然语言 证明是错误的 ，这份证明 仍需独立核查正确 性 。 开发可靠的方法来检查 数学 证明本身 ，即将自然语言 转化为形式语言的过程 正 变得尤为重要。 SAIXIANSHENG AI找到的答案，或并非数学家关心的问题 除了证明 语言翻译过程 的差异， OpenAI 此次 给出的证明思路 也引发了数学界讨论。 N-S 方程的核心问题之一是：在三维空间中，如果流体从一个光滑、能量有限的初始状态出发，其运动是否始终能够保持光滑？还是说，在某个有限时刻，流体速度可能变得无穷大，形成所谓的 “ 奇点 ” ？ 此次 OpenAI 内部的模型找到了奇点出现的构造，它可以被看作一种向内部旋转的流体漩涡。初始静止的流体受到光滑外力的作用，在运动过程中像意大利面一样沿轴向不断拉长。随着中心区域收缩，局部速度不断增大，在某一有限时刻变得无界，形成奇点，但流体能量仍然保持有限。 这一构造的关键是 N-S 方程中描述流体运动的各项因素，如加速度、压力梯度以及黏性项等都必须在数值急剧增大时仍以精确的方式相互抵消，使外力始终保持光滑。 OpenAI 证明了，在静止状态下初始平滑的流体，可以在有限时间内形成奇点。这涉及克雷研究所问题表述中允许带光滑外力的两条证明路线。 如果 证明 无误 ，