人类数学家的反击：N-S方程证明正确性存疑

导读： OpenAI宣称解决纳维-斯托克斯方程（Navier-Stokes equations，简称N-S方程）问题近两个月后，数学界仍未就OpenAI是否真正解决这一问题达成共识。截至11月2日，N-S方程问题在克雷研究所官网上尚未被列为“已解决问题”。 10月6日，伦敦国王学院应用数学讲师亚历山大·巴斯图尼斯（Alexander 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形式化版本中公式的上界依赖新增了梯度项AR。 研究人员认为，这些差异意味着，Lean形式化并没有逐项准确验证自然语言论文的全部证明，而是验证了更宽松条件下的数学命题。 此前，OpenAI发布的信息显示，其模型GPT-6 Astra耗时17小时，将证明形式化为Lean代码并验证。 提出质疑的三位作者之一奇尔切利表示，“我们的论文利用可解性复杂度指数（SCI）层级和逻辑工具，揭示了AI在形式化工作中的局限性。” 需要指出的是，研究人员并没有因此证明OpenAI的自然语言证明是错误的，这份证明仍需独立核查正确性。 开发可靠的方法来检查 数学 证明本身 ，即将自然语言 转化为形式语言的过程 正 变得尤为重要。 SAIXIANSHENG AI找到的答案，或并非数学家关心的问题 除了证明 语言翻译过程 的差异， OpenAI 此次 给出的证明思路 也引发了数学界讨论。 N-S方程的核心问题之一是：在三维空间中，如果流体从一个光滑、能量有限的初始状态出发，其运动是否始终能够保持光滑？还是说，在某个有限时刻，流体速度可能变得无穷大，形成所谓的“奇点”？ 此次OpenAI内部的模型找到了奇点出现的构造，它可以被看作一种向内部旋转的流体漩涡。初始静止的流体受到光滑外力的作用，在运动过程中像意大利面一样沿轴向不断拉长。随着中心区域收缩，局部速度不断增大，在某一有限时刻变得无界，形成奇点，但流体能量仍然保持有限。 这一构造的关键是N-S方程中描述流体运动的各项因素，如加速度、压力梯度以及黏性项等都必须在数值急剧增大时仍以精确的方式相互抵消，使外力始终保持光滑。 OpenAI证明了，在静止状态下初始平滑的流体，可以在有限时间内形成奇点。这涉及克雷研究所问题表述中允许带光滑外力的两条证明路线。 如果 证明 无误 ， O penAI 确实 解决 了 N -S 方程 问题。 图：局部不可压缩运动的示意图。橙色表示较快的角速度；青色表示较慢的角速度。流速也取决于半径大小。轨迹呈现出向内螺旋式运动和轴向拉伸的现象。图源：https://openai.com/index/navier-stokes-solution/ 据《科学美国人》报道，芝加哥大学数学家路易斯·西尔维斯特（Luis Silvestre）表示，“N-S方程中的黏性问题已经解决，但OpenAI给出的证明借助外力，这与我们真正想解决的问题不