OpenAI宣称解决纳维-斯托克斯方程（Navier-Stokes equations，简称N-S方程）问题[1]近两个月后，数学界仍未就这一问题是否真正被解决达成共识。在克雷研究所官网，N-S方程仍被列为“未解决问题”[2]。
菲尔兹奖得主邓煜10月25日在“知识分子”“赛先生”论坛发表演讲时提到，某AI公司10月6日公布涉及300多个问题的700多篇文章，以及更早前公布千禧年问题中Navier-Stokes方程的证明，无疑在数学界产生了非常重大的影响。邓煜说，这些论文对数学有相当大的促进作用，与此同时，某AI公司很多情况下没有公布证明的思维链，也未说明是否基于其他人的思路，而且在没有任何正确性保证的情况下就直接发布。
值得一提的是，《知识分子》此前报道，六位数学家创建了“数学之舵”论坛(mathhelm.org)，欢迎全球数学研究者一起讨论OpenAI的722篇论文，以及AI生成的其他论文。
OpenAI首席执行官山姆·奥特曼（Sam Altman）则在10月29日接受Cheeky Point访谈时表示，证明N-S方程花了大约一千万美元，而OpenAI已在数学问题上投入了数以亿计的美元，还有大量发现未公开。他还称，希望找到一个可行的解空间(solution space)：既能让全社会从这些知识中获益，也能让各领域从业者拥有尽可能理想的未来。
撰文｜李璐
● ● ●
人类数学家，对OpenAI发布的Navier-Stokes方程证明的正确性提出质疑。
10月6日，伦敦国王学院应用数学讲师亚历山大·巴斯图尼斯（Alexander Bastounis）、剑桥大学博士法比安·奇尔切利（Fabian Circelli）和教授安德斯·汉森（Anders C. Hansen）在arXiv网站发布论文[3]，认为对于N-S方程的证明，OpenAI公开的自然语言证明与Lean形式化证明存在不一致。
10月27日，伦敦国王学院新闻中心以“OpenAI的N-S证明遭到质疑”（OpenAI's Navier-Stokes proof called into question）为题做了报道[4]。亚历山大・巴斯图尼斯博士表示：“OpenAI难以把它的证明准确转换成机器可核验语言，这凸显了一个更普遍的难题：验证AI输出结果的正确性，依旧极其困难。”
这大概意味着，OpenAI公布的计算机验证结果，并不能直接证明其面向人类读者的数学论文正确。
此前，OpenAI还被质疑或使用未公开的人类数学家研究思路以及数据，并在研究尚未充分核查的情况下抢先发布仓促的证明。9月11日，陶哲轩、邓煜等25位菲尔兹奖得主曾发表联署声明《人工智能在数学领域的严重错位》（A Severe Misalignment of AI in Mathematics）。
01
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代码并验证。
前述质疑论文的共同作者法比安·奇尔切利表示，“我们的论文利用可解性复杂度指数层级和逻辑工具，揭示了AI在形式化工作中的局限性。由此我们可以预判AI自动形式化在现实中将会遇到、也确实正在遇到各类困难。”
另一位共同作者、剑桥大学数学教授安德斯・汉森说：“计算数学的基础理论，对于理解AI的能力与局限至关重要。”
需要指出的是，研究人员并未因此证明OpenAI的自然语言证明是错误的，这份证明仍需独立核查正确性。实际上，开发可靠的方法来检查数学证明本身，即将自然语言转化为形式语言的过程正变得尤为重要。
02
“这与我们真正想解决的问题不同”
除了证明语言翻译过程的差异，OpenAI此次给出的证明思路也在数学界引发激烈讨论。
N-S方程核心问题之一是：在三维空间中，如果流体从一个光滑、能量有限的初始状态出发，其运动是否始终能够保持光滑？还是说，在某个有限时刻，流体速度可能变得无穷大，形成所谓的“奇点”？
局部不可压缩运动的示意图。橙色表示较快的角速度；青色表示较慢的角速度。流速也取决于半径大小。轨迹呈现出向内螺旋式运动和轴向拉伸的现象。图源：OpenAI
此次OpenAI内部的模型找到了奇点出现的构造，它可以被看作一种向内部旋转的流体漩涡。初始静止的流体受到光滑外力的作用，在运动过程中像意大利面一样沿轴向不断拉长。随着中心区域收缩，局部速度不断增大，在某一有限时刻变得无界，形成奇点，但流体能量仍然保持有限。
这一构造的关键是N-S方程中描述流体运动的各项因素，如加速度、压力梯度以及黏性项等都必须在数值急剧增大时仍以精确的方式相互抵消，使外力始终保持光滑。
OpenAI证明了，在静止状态下初始平滑的流体，可以在有限时间内形成奇点。这涉及克雷研究所问题表述中允许带光滑外力的两条证明路线。如果证明无误，OpenAI确实解决了N-S方程问题。
据《科学美国人》报道，芝加哥大学数学家路易斯·西尔维斯特（Luis Silvestre）表示，“N-S方程中的黏性问题已经解决，但OpenAI给出的证明借助外力，这与我们真正想解决的问题不同。” [5]
马德里金融研究大学数学系教授路易斯·索罗亚（Luis Martínez-Zoroa）也表示，大多数数学家在思考N-S方程时，并没有这一初始外力。他们希望找到流体中的内在力，以一种更纯粹、更本质的方式到达奇点。
据《纽约客》报道，陶哲轩在加州理工学院演讲时，一位观众观察到AI迄今为止一直在解决已有的问题，因此提出疑问，新的问题从何而来。陶哲轩回答，“新的问题要在缓慢且深思熟虑的过程中诞生，而这个过程正在被摧毁。
参考文献：
[1]https://openai.com/zh-Hans-CN/index/navier-stokes-solution
[2]https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
[3]https://arxiv.org/pdf/2610.08144
[4]https://www.kcl.ac.uk/news/openais-navier-stokes-proof-called-into-question
[5]https://www.scientificamerican.com/article/did-openai-solve-the-wrong-navier-stokes-problem/
本文原载于“赛先生”
0
推荐
京公网安备 11010502034662号 
