人类数学家的反击：N-S方程证明正确性存疑
OpenAI宣称解决纳维-斯托克斯方程（Navier-Stokes equations，简称N-S方程）问题近两个月后，数学界仍未就OpenAI是否真正解决这一问题达成共识。截至11月2日，N-S方程问题在克雷研究所官网上尚未被列为“已解决问题”。
图源：pixabay 10月6日，伦敦国王学院应用数学讲师亚历山大·巴斯图尼斯（Alexander Bastounis）、剑桥大学博士法比安·奇尔切利（Fabian Circelli）和安德斯·汉森（Anders C. Hansen）在arXiv网站上发布论文，指出对于N-S方程的证明，OpenAI公开的自然语言证明与Lean形式化证明存在不一致。 这意味着，OpenAI公布的计算机验证结果，并不能直接证明其面向人类读者的数学论文正确。
论文《Navier–Stokes lost in translation》图源：参考文献[1] 此前，OpenAI还被质疑或使用了未公开的人类数学家研究思路以及数据，并在研究尚未充分核查的情况下抢先发布了一份仓促的证明。《赛先生》曾梳理过相关人类数学家与AI公司的互动过程。 此次，人类数学家对OpenAI发布的该证明的正确性提出质疑。 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的自然语言证明是错误的，这份证明仍需独立核查正确性。开发可靠的方法来检查数学证明本身，即将自然语言转化为形式语言的过程正变得尤为重要。 AI找到的答案，或并非数学家关心的问题 除了证明语言翻译过程的差异，OpenAI此次给出的证明思路也引发了数学界讨论。 N-S方程的核心问题之一是：在三维空间中，如果流体从一个光滑、能量有限的初始状态出发，其运动是否始终能够保持光滑？还是说，在某个有限时刻，流体速度可能变得无穷大，形成所谓的“奇点”？ 此次OpenAI内部的模型找到了奇点出现的构造，它可以被看作一种向内部旋转的流体漩涡。初始静止的流体受到光滑外力的作用，在运动过程中像意大利面一样沿轴向不断拉长。随着中心区域收缩，局部速度不断增大，在某一有限时刻变得无界，形成奇点，但流体能量仍然保持有限。 这一构造的关键是N-S方程中描述流体运动的各项因素，如加速度、压力梯度以及黏性项等都必须在数值急剧增大时仍以精确的方式相互抵消，使外力始终保持光滑。 OpenAI证明了，在静止状态下初始平滑的流体，可以在有限时间内形成奇点。这涉及克雷研究所问题表述中允许带光滑外力的两条证明路线。如果证明无误，OpenAI确实解决了N-S方程问题。
图：局部不可压缩运动的示意图。橙色表示较快的角速度；青色表示较慢的角速度。流速也取决于半径大小。轨迹呈现出向内螺旋式运动和轴向拉伸的现象。图源：https://openai.com/index/navier-stokes-solution/ 据《科学美国人》报道，芝加哥大学数学家路易斯·西尔维斯特（Luis Silvestre）表示，“N-S方程中的黏性问题已经解决，但OpenAI给出的证明借助外力，这与我们真正想解决的问题不同。” 马德里金融研究大学数学系教授路易斯·索罗亚（Luis Martínez-Zoroa）也表示，大多数数学家在思考N-S方程时，并没有这一初始外力。他们希望找到流体中的内在力，以一种更纯粹、更本质的方式到达奇点。 据《纽约客》报道，陶哲轩在加州理工学院演讲时，一位观众观察到AI迄今为止一直在解决已有的问题，因此提出疑问，新的问题从何而来。陶哲轩回答，“新的问题要在缓慢且深思熟虑的过程中诞生，而这个过程正在被摧毁。