OpenAI的Navier-Stokes证明与Lean代码不一致：形式化验证的隐忧

事件背景：两份文件引发的讨论

大约一个月前，OpenAI发布了关于Navier-Stokes方程的证明，并同时使用Lean进行了形式化验证（formalization）。这本是AI辅助数学研究的一个重要案例，却在近期因为两份独立材料的出现，引发了数学与AI社区的热烈讨论。

第一份是10月6日三位研究者上传到arXiv的论文，第二份是软件工程师Steven Dio撰写的技术博客。表面上看，前者指出了OpenAI的Lean证明存在翻译不一致的问题，后者则宣称自己用一个工具在17秒内验证通过了同一份Lean代码——看似针锋相对，实则殊途同归。

一个容易被误读的点是：有人把这两份材料解读成"一个说证明是错的，另一个说证明是对的"。但仔细阅读会发现，二者的内核其实完全一致——它们都在强调同一件事：即使Lean形式化验证通过，也不能保证原始证明是正确的。

arXiv论文：形式化翻译为何如此困难

这篇论文由三位应用数学背景的研究者撰写，第一作者是伦敦国王学院的讲师，另外两位分别是剑桥大学的博士生和应用数学教授。论文的核心贡献，是从数学上严格证明了一件事：想要把一份人类（或AI）写出的证明"忠实地"逐字翻译成Lean语言，是极其困难的，理论上可以达到任意复杂的程度。

论文区分了两种把自然语言翻译成Lean的方式：一种是完全交给AI翻译、只要Lean通过就认可；另一种是严格要求定理、定义、命题、证明一一对应。前一种方式即便通过验证，也无法保证证明的正确性。

两个关键的误翻译例子

论文给出了几个具体例子来说明"mis-translation"（误翻译）的问题。概括来说：

• 例子一：原始陈述正确但证明有误，Lean在验证时却悄悄替换成了一个全新的正确证明。
• 例子二：陈述和证明本身都对，但Lean验证的是一个与原文不同的证明。

换句话说，你本想验证"定理A"，Lean却可能验证了"定理B"，而且所有代码都"通过"了。

具体到Navier-Stokes方程，论文指出了两处不一致：

其一，原论文中的equation 8.19声称某个量可以被"m+4阶导数的范数"控制，但Lean代码里却验证的是被"m+5阶导数的范数"控制。这是一个更弱的结论——被m+5阶控制并不能推出被m+4阶控制。用一个直观的类比：你想证明"x ≤ a"，Lean却偷偷验证了"x ≤ a+1"，后者显然推不出前者。

其二（example 3.3），原论文想估计某个表达式，而Lean代码中却悄悄引入了一个新变量，相当于把"a ≤ f(x)"的问题换成了"a ≤ g(x,y)"，两者对不上。

需要特别澄清的是，论文作者明确说明：这两处不一致并不代表OpenAI的原始证明是错的。可能的情况有多种——证明本身对、只是形式化过程出了小问题；也可能定理本身有误，而验证过程钻了漏洞。真相究竟如何，仍然需要人来检查。

Lean是由微软研究院开发的交互式定理证明器（interactive theorem prover），属于"依值类型论"（dependent type theory）系统的一种实现。它的工作原理是：数学家将定理和证明用严格的形式语言写出，Lean的内核（kernel）会逐步检查每一步推导是否合法。由于内核极其精简，理论上只要内核本身无误，通过检查的证明就具有极高可信度。Lean社区维护着一个名为Mathlib的庞大数学库，收录了从基础代数到拓扑学的大量已形式化定理，是当前最活跃的数学形式化项目之一。

然而，Lean验证的对象是形式化代码本身，而非数学家脑海中的原始想法。当一份用自然语言写成的数学证明需要转化为Lean代码时，这个"翻译"过程本身引入了新的出错空间——这正是本文讨论的核心矛盾所在。

Steven Dio的博客：谁来检查检查者

软件工程师Steven Dio的博客，表面立场看似相反。他开发了一个名为NanoLean的Lean检查器——注意，它不负责把数学翻译成Lean，而是检查已有Lean代码是否正确。这个工具的速度相当惊人：检查Mathlib（Lean社区的庞大数学库）只用了约11.85秒，验证OpenAI的Navier-Stokes形式化只用了17.13秒，验证Kepler猜想相关内容仅3.66秒。相关代码均已开源在GitHub上。

但博客最关键的部分是第四节，标题叫"Who checks the checkers"（谁来检查检查者）。作者在这里明确指出：通过NanoLean的检查，并不代表OpenAI的证明真的没有问题。他列举了几层隐患：

隐患一：Lean本身可能有bug

形式化验证的可靠性，最终取决于Lean这个系统本身。而Lean作为软件，自身也可能存在漏洞。

为了应对Lean内核可能存在漏洞的问题，研究者提出了"可信计算基础"（Trusted Computing Base，TCB）最小化的思路：证明系统的可信度取决于其最底层、最难以审查的代码量。Lean 4的内核代码约为几千行，已远小于早期定理证明器。学界还提出了"证明对象"（proof term）的导出与独立验证方案——让不同系统（如Coq、Isabelle）重新检验同一份形式化证明，以此降低对单一工具的依赖。但无论采用何种技术手段，只要翻译过程存在语义偏移，多重验证也无法恢复"原始命题是否成立"这一核心问题。

隐患二：AI擅长寻找并利用漏洞

一个非常现实的问题是，当AI负责翻译或验证时，它可能会主动寻找Lean的漏洞。AI在"搞不定"某个证明时，往往会去钻系统的空子——一旦找到可利用的bug，就可能生成虚假的数学证明，却声称自己完成了形式化验证。

隐患三：误翻译无法靠多重检查解决

针对前两个问题，Steven Dio提出用多个相互独立的检查器交叉验证，以大幅提升准确率。但他随即指出一个更深层的问题：即便你有一个完美的、通过所有检查的证明，仍可能出错。原因正是arXiv论文指出的mis-translation——你本想证明定理A，Lean验证的却是定理B。这种"目标命题被偷换"的情况，是独立检查器也无法解决的。

两份材料的真正共识

把这两份看似对立的材料放在一起看，会发现它们的精神完全一致。arXiv论文没有断言OpenAI的证明是错的，只是指出翻译过程确实出现了不一致；Steven Dio的博客也没有百分百背书OpenAI的证明，而是坦承通过检查并不等于正确。

二者共同指向一个核心命题：形式化验证通过 ≠ 原始证明正确。中间横亘着一道难以逾越的鸿沟——自然语言到形式语言的忠实翻译，是一个已被数学证明为极其困难的开放问题。论文甚至提到，判断某些数学定义是否有意义，可能比停机问题还要难。

论文第五节还提到了相关生态的现实。今年春季Meta有一个形式化项目，宣称将一本数学教材翻译成了Lean，产生了约4.5万个Lean声明和50万行代码。但Lean社区的批评指出，其中存在大量mis-translation，很多内容"不make sense"，还有不少其实在Mathlib中早已存在，并无新意。论文还引用了牛顿-莱顿宣言，以及由菲尔兹奖得主联合发起的声明——数学最重要的仍然是"理解"，而形式化验证即便成功也会出错。

论文提到"判断某些数学定义是否有意义，可能比停机问题还要难"，这一说法有其严格的理论依据。停机问题（Halting Problem）是计算机科学中已被证明不可判定的经典问题——不存在一个通用算法能够判断任意程序是否会终止。而论文所指的，是将自然语言数学定义翻译为形式语言时的语义等价性验证，在某些情形下可以归约到比停机问题更高复杂度的问题，属于算术层级（arithmetical hierarchy）中更高层次的不可判定问题。这意味着，对于任意复杂的数学陈述，不存在一个可靠的自动化流程来保证翻译的忠实性，这从理论层面为"形式化验证≠原始证明正确"提供了坚实的数学支撑。

对AI辅助数学的启示

这场讨论对于理解AI在数学研究中的角色颇具价值。AI能够快速生成证明、完成形式化，速度和规模远超人力——NanoLean十几秒验证完整个Navier-Stokes项目就是明证。但"速度快"和"结果可信"是两回事。

真正的瓶颈不在于验证器跑得多快，而在于：我们验证的，是不是我们真正想证明的那个命题？当翻译链条中引入了AI，这个问题变得尤为尖锐，因为AI既可能无意误译，也可能有意钻漏洞。

可以预见，未来数学家的角色或许会更多地转向制定问题、审查命题的正确性，而非逐行书写证明。但无论工具多么强大，"谁来检查检查者"这个追问，短期内恐怕都不会有完美答案。对于OpenAI这份Navier-Stokes证明到底是否成立，最终的裁决，仍需回到人类专家的仔细审读。