OpenAI 在 Navier-Stokes 证明过程中，错误将数学公式翻译成了代码

计算机说"证明通过"，就一定意味着证明是对的吗？三位数学家给出了一个令人意外的答案。

数学家亚历山大·巴斯图尼斯、法比安·奇尔切利和安德斯·汉森近日在预印本平台arXiv上发表论文，矛头直指OpenAI此前高调宣布的纳维-斯托克斯方程证明。

论文标题颇为醒目，叫作《纳维-斯托克斯迷失在翻译中》。副标题则直接点明了核心观点，AI自动形式化的Lean验证，并不能保证自然语言证明的正确性。

作者在论文中指出，经过形式化的Lean证明，"并不对应"那份关于纳维-斯托克斯方程解爆破的自然语言证明。

换句话说，被计算机检验通过的，可能并不是数学家真正想证明的那个东西。

这一质疑，直接触及了当下AI数学研究中一个被寄予厚望的"安全网"。

论文作者之一安德斯·汉森长期研究计算的根本极限问题，此前就曾从数学上论证过深度学习方法在某些问题上存在内在的不稳定性。

一场备受瞩目的"证明"

故事要从今年9月说起。9月8日，OpenAI宣布其智能体解决了纳维-斯托克斯方程的一个问题，证明了方程的解会出现"爆破"，并附上了一份Lean形式化证明。

纳维-斯托克斯方程是描述流体运动的基本方程，从天气预报到飞机设计，从血液流动到海洋洋流，都离不开它。

它的三维情形是否总存在光滑解，是克雷数学研究所悬赏百万美元的七大千禧年难题之一。

所谓"爆破"，指的是方程的解在有限时间内变得无穷大，就像一个平静流动的漩涡突然在某一点"失控"。证明或否定这类现象，一直是数学家们梦寐以求的目标。

OpenAI的这一宣布本身就伴随着争议。

就在前一天，纽约大学数学家特里斯坦·巴克马斯特刚刚公布，他与合作者莱旺·阿尔波热在这一问题上取得了进展。巴克马斯特对OpenAI宣布的时机提出了质疑，OpenAI则否认在攻关期间看过两人尚未发表的工作。

Lean为何被视为"终极裁判"

要理解这篇新论文的分量，先得了解Lean是什么。

Lean是一种交互式定理证明工具。数学家可以把证明的每一步都写成严格的代码，由计算机逐行检查逻辑是否成立。

近年来，数学界已经用Lean完成了一批重要定理的形式化，并建立起庞大的数学知识库，Lean也因此成为数学家与AI合作的重要桥梁。

只要代码编译通过，就说明在给定的定义和假设下，结论在逻辑上无懈可击。正因为如此，Lean被视为验证AI数学成果的"终极裁判"。

AI生成的证明往往冗长晦涩，人工审读费时费力，还容易漏掉细微的错误。如果能把证明翻译成Lean代码并通过检验，似乎就能一劳永逸地建立信任。

这个把自然语言数学翻译成形式语言的过程，被称为"自动形式化"。

OpenAI在发布纳维-斯托克斯证明时附上Lean文件，在最近公布的722篇数学论文中也承诺陆续补充Lean证明，正是基于这样的逻辑。

问题出在"翻译"这一步

巴斯图尼斯、奇尔切利和汉森的论文，恰恰瞄准了这个逻辑链条中最容易被忽视的一环，翻译。

他们指出，Lean检验通过，只能说明Lean代码本身是自洽的，却不能说明这段代码忠实地表达了原来的自然语言证明。

这就好比把一本中文小说翻译成英文。英文版语法完美、逻辑通顺，但如果翻译时悄悄改动了某个关键情节，那它讲的就已经是另一个故事了。

数学语言天然带有大量隐含约定和模糊之处。一个定义的细微差别、一个变量范围的不同理解，都可能让形式化后的命题与原意产生偏差。

论文作者从理论层面论证，要忠实完成自动形式化，需要消除自然语言文本中的种种歧义，而这项任务在"可解性复杂度指数"层级中处于最高层。

用通俗的话说，作者认为，忠实的AI自动形式化在计算意义上比任何计算问题都难，甚至比著名的"停机问题"还要难。

论文还给出了多个实际案例，展示AI把自然语言命题和证明错误翻译成Lean代码，导致自然语言证明与其Lean"验证"之间出现不匹配。OpenAI宣布的纳维-斯托克斯证明，就被列为其中之一。

对AI数学热潮的一记提醒

这篇论文目前仍是预印本，尚未经过同行评审，OpenAI方面也尚未就具体质疑作出详细回应。

但它提出的问题，值得整个领域认真对待。近一年来，AI在数学研究中的表现突飞猛进，从解决埃尔德什问题到批量生成数百篇论文，Lean形式化被普遍视为建立信任的关键手段。

如果形式化本身就可能"翻译走样"，那么单靠一句"已通过Lean验证"，显然不足以让人放心。

这并不意味着Lean没有价值。恰恰相反，它依然是目前最可靠的数学验证工具之一。

问题在于，人们需要更加审慎地检查形式化后的命题，是否真的就是想要证明的那个命题。这一步，至少在目前，仍然离不开人类数学家的眼光和判断。

陶哲轩此前也多次提醒，AI生成的证明可能表面无懈可击，却暗藏难以察觉的细微错误。

科学的进步，从来不是靠某一种工具一锤定音，而是靠层层把关、反复检验。

在AI以惊人速度"生产"数学证明的今天，这篇论文像是一记及时的提醒。机器可以帮助人类走得更快，但确认方向是否正确的那双眼睛，仍然要由人来守住。