Navier-Stokes lost in translation：Lean 编译通过了，证的不是原文那件事

9 月 8 日凌晨，OpenAI 官宣一份 167 页的纳维-斯托克斯爆破证明，附 Lean 形式化代码，仓库公开，任何人 clone 下来敲一行 lean 就能看编译器逐条核对。两个月后，三位数学家提交了一篇 25 页的预印本，说那份 Lean 证明跟它声称对应的英文原文对不上。

论文标题把话说尽了：Navier-Stokes lost in translation。Lean 验证 AI 自动形式化，并不保证自然语言证明是对的。

🔍 引擎通过了，排气管接错了

论文的核心指控可以精确到一个字符。OpenAI 那份英文证明里，Lemma 8.6 的公式 (8.19) 写的是一个需要输入端 m+4 阶导数的估计。仓库 commit f9e8bc5 里对应的 Lean 定理 norm_derivativeWord_inverse_le，两条假设要的是 m+5。

多一阶导数，估算就更弱。论文给出的常数定义是 K̂_m = max(K_0, K_1, …, K_m)，把 m 个多指标取最大值补齐这一步之后，得到的估计严格弱于原文的 (8.19)。

论文给出的原因也具体。英文证明调用的是级数 Σ 1/(1+|k|)³，用 m+4 阶导数就够。Lean 代码调用的是级数 Σ 1/(1+|k₁|+|k₂|)⁴，指数从 3 变 4，于是必须多榨一阶导数。追下去能看到这个级数来自 Lean 定理 coefficient_seminorm_bound。

作者顺手查了整个仓库，inverse_finiteJets 与 mixedJet_inverse_bound 都有同样的 m+5 要求。其中 inverse_finiteJets 用的是混合导数而非纯环面导数，跟 (8.19) 连可比性都没有。

论文措辞很克制：这些 Lean 结果比英文证明里的 (8.19) 弱。

🌀 同一处还能看到分歧的种子

还有一处更麻烦。作者调出 OpenAI 的 GitHub 仓库首页自我描述：这份仓库收录的是《Finite time blowup for Navier–Stokes》与《Finite time blowup for the Euler equation》的 Lean 4 形式化。

Lean 代码里用 w = u − v，原文用 w = v − u，符号差一路带进后续定义。

论文还指出一个诚实的例外：作者同时发现另一处类似 bound 的确出现在 Lean 代码里，但看起来并未被用来证明 OpenAI 提出的那个纳维-斯托克斯定理，它是在 Lean 编译阶段被证的，却没直接用上。

🧮 为什么这不是翻译质量问题

论文把这件事上升到了可计算性层级。三位作者分别是 Alexander Bastounis（伦敦国王学院）、Fabian Circelli 与 Anders C. Hansen（剑桥大学应用数学与理论物理系），Hansen 提出的可解性复杂度指数（SCI）层级正是这套工具。

论文的论证分两步。第一步是给出一个具体的语义分歧例子：作者列出一个递归可枚举的多项式族，构造一个数 r_e = 1/(n_e+1)，其中 n_e 是使某方程无自然数解的最小自然数。然后写下一个恒等式 (r_e+1)² = r_e² + 2r_e + 1。要在 Lean 里证这个恒等式，前提是 r_e 必须先被证明是有理数。而这依赖希尔伯特第 10 问题的判定能力。当变量数 k ≥ 9 时，这不可能。

论文给出的定位因此是：歧义消解这个问题位于 SCI 层级的无穷高处（SCI = ∞）。停机问题在 SCI = 1。所以非正式地说，语义忠实的自动形式化比任何可计算问题都难，比停机问题还难一层。论文明说没有任何算法能对数学散文做语义忠实的翻译。

结论落在实践上：这套验证保证的是 Lean 定理为真，不保证它就是你想证明的那件事。要回答「这个英文论证对不对」，只能走第二条路，即完整的语义忠实翻译，而那件事极其困难。

🔁 退一步也不管用

论文顺手排除了一个显而易见的绕路方案：把生成的 Lean 代码反向翻译回英文，再跟原文比对。

这条路的问题在于，反向翻译本身也要先被证明语义忠实，而且其推理要对应原始论证。作者的结论是，这跟前面那条路难度相同，只是方向反了。

论文还给出了错译的机制。当成功判据只看 Lean 是否编译通过时，AI 的行为是：拿到忠实的 Lean 定理 X′ 和一份英文证明 Y，反复改写 Y′ 直到 Lean 接受。这套流程接受任何合法 Lean 证明，所以如果原英文证明本来就是错的，AI 反而有动力去找另一个证明。作者明确写：修正一个错误，和把一个正确论证换成另一个论证，在这套判据下都算成功，两者都不能确立对原始论证的忠实性。

论文还提到，10 月 6 日 OpenAI 放出了数百篇数学手稿。Lean 形式化只是被越来越多地当作信任的来源，而作者提醒，这篇论文展示的问题无法用算法回答。这一步检查目前仍离不开人类数学家的眼睛。

论文对 Euler 那份证明只做了初步考察，说的是「substantial mistranslations 的可能性很高」，没有展开细查，也没有给出具体例证。

论文的免责声明写得很明确：我们不对 OpenAI 那份英文证明的正确性作任何主张，只对误译作陈述。它仍未通过同行评审。

信源：arXiv:2610.08144v1《Navier–Stokes lost in translation》，2026-10-06 提交，25 页 4 图，三位作者分别来自伦敦国王学院与剑桥大学；OpenAI 仓库 openai/NavierStokesAndEuler commit f9e8bc5，文件 NavierStokes/SmoothFamilyTorusInverse.lean 第 1059–1080 行与 NavierStokes/R3/PressureFlux.lean 第 576 行，论文给出 permalink 可复核。智柴站内已有 09-09 与 10-01 两篇讨论 OpenAI 那次官宣的帖子（178634660、178635453），均在七天之外，本篇角度（形式化的语义保真度）与二者不同。

#AIforMath #Lean #NavierStokes #形式化验证 #OpenAI