新论文称 Lean 验证不能为 OpenAI 的 Navier-Stokes 自然语言证明背书

这篇论文试图解决的核心问题是：为什么通过 Lean 交互式定理证明器机械验证 AI 自动形式化（AI Autoformalisation）的结果，并不能保证原始自然语言数学证明的正确性。

• 问题场景与现实重要性：自动形式化正日益被用于检验复杂的数学论证。例如 OpenAI 宣布利用 AI 形式化验证了三维不可压缩纳维-斯托克斯方程解的有限时间爆破。在这一流程中，形式化语言（如 Lean）代码编译通过常被视作原自然语言证明无误的背书。
• 现有认知的核心漏洞：作者指出，将自然语言证明翻译为 Lean 代码时，系统的成功标准通常仅仅是“Lean 接受翻译并成功编译（无 sorry 关键字且不引入额外公理）”。这种准则仅能确认形式化目标命题自身成立，完全无法保证翻译过程在语义上忠实（Semantically Faithful）。
• 核心论点与理论发现：作者提出，为了实现语义忠实的翻译，AI 必须消解自然语言中的歧义与隐藏预设；作者证明，在数学文本中判定这类歧义和预设是否良定，其计算复杂度在可解性复杂度指数（Solvability Complexity Index, SCI）层级上可以达到无穷大（SCI = ∞），因此在理论上比停机问题（Halting problem，其 SCI = 1）更加困难。
• 论文的主要贡献：论文划分了两类自动形式化任务，建立了语义忠实形式化的理论不可计算性屏障，并通过实例（包括 OpenAI 宣称的纳维-斯托克斯方程爆破证明及 Meta 的教材翻译项目）展示了 AI 自动形式化在实践中发生的严重语义误译与证明脱节。

论文在相关背景和理论渊源中讨论了以下研究工作：

• 自然语言与形式语言的语义理论：论文追溯了逻辑学、语言学与哲学界关于自然语言到形式语言转换及语义保持的长期讨论，引用了 Tarski（1944）关于真理的语义概念、Montague（1970, 1974）将英语作为形式语言与通用语法的开创性工作、Quine（1959, 1970）关于翻译不确定性的理论，以及 Moschovakis（2006）、Berto & Hornischer（2023）关于认知同义与意义微积分的讨论。此外，论文提及 Hales（2019）提出的在数学中采用受控自然语言（Controlled Natural Languages）的主张。
• 计算理论与可解性复杂度指数（SCI）层级：论文的理论证明建立在 Hansen（2011）以及 Ben-Artzi 等人（2015, 2020）、Colbrook & Hansen（2022）等发展的 SCI 层级基础之上，该体系继承了 Smale（1981, 1997）计算复杂性与多项式求根的基础研究纲领。同时，论文引用了 Matiyasevich（1993）对希尔伯特第十问题的解决、Jones（1982）关于九未知数丢番图方程的精细化结果，以及 Sun（2026）关于整数未知数的最新进展。
• 大规模数学自动形式化项目：论文讨论了工业界近期尝试，包括 Meta（Rammal 等，2026）声称自动形式化 26 本数学教材、产出 4.5 万条声明的 Atlas 项目；以及 Anthropic（Buzzard，2026）对费马大定理形式化所产出的 1300 万行 Lean 代码。同时提及 2026 年学界的《莱顿声明》（Leiden Declaration）与 25 位菲尔兹奖得主发起的《数学中 AI 的严重对齐失准》（A Severe Misalignment of AI in Mathematics）声明对形式化失准风险的警告。
• 流体力学奇点问题背景：论文以 Navier-Stokes 与 Euler 方程的有限时间爆破为应用案例，引用了 Leray（1934）、Caffarelli-Kohn-Nirenberg（1982）、Fefferman（2006 年千禧年问题描述）、Tao（2016）、Hou（2023）以及 Elgindi（2021）、Chen & Hou（2022, 2025）等工作，并直接将 OpenAI（commit f9e8bc5）公开的 Lean 4 仓库与自然语言手稿进行比对。

作者认为，现有实践普遍忽视了形式化成功（可编译）与语义忠实之间的鸿沟，本文首次从 SCI 层级奠定了语义忠实不可计算性的理论基础，并首次针对 OpenAI 的爆破证明给出了具体的形式化脱节证据。

作者从概念辨析、理论复杂度刻画和实际误译剖析三个层面展开论证。

两类自动形式化任务的形式化区分

论文将从自然语言（NL）到形式语言（如 Lean）的自动形式化区分为两类不同任务：

• 任务 (i)：翻译推称的 NL 证明以获得形式化 Lean 证明：给定已正确翻译的定理目标命题与一份声称的 NL 证明，AI 的目标是生成一份 Lean 接受并成功编译的代码（不允许使用 sorry 占位符或额外公理）。只要编译通过即宣告成功。
• 任务 (ii)：数学文本的语义忠实翻译：要求对文本中的每一个定义、定理、命题和证明步骤进行翻译，并在语义上严格保全原始数学内涵和概念依赖关系。作者指出，任务 (i) 的成功绝不蕴含任务 (ii) 的达成。

核心论证：歧义消解与预设验证在 SCI 上的不可解性

作者指出，判断数学文本中一个对象的良定性可能依赖于未决的计算问题。

• 构造带有存在性预设的算术命题：构造整系数多项式递归枚举 p_e，定义谓词 B_e(n) \Longleftrightarrow \forall (x_1,\dots,x_k) \in \mathbb{N}^k, p_e(n, x_1,\dots,x_k) \neq 0。定义 n_e 为使得 B_e(n) 成立的最小自然数，并定义有理数 r_e = 1/(n_e + 1)。
• 判定良定性的算术复杂度：欲验证等式 (r_e + 1)² = r_e² + 2r_e + 1，形式化系统必须判定 n_e 是否存在（即 r_e 是否良定）。作者利用 DPRM 定理及其 9 未知数精细化结果（Jones, 1982）证明：在 k ≥ 9 时，集合 d := {e ∈ ℕ : ∃ n ∈ ℕ, B_e(n)} 是 Σ⁰₂-完全的（Theorem A.3）。即使拥有停机问题的预言机（Oracle），也无法判定 n_e 是否良定。
• 推广至任意算术层级与 SCI = ∞：作者将谓词推广至交替量词结构 B_e^(l)(n)，证明判定对应指标的存在性集合 d_l 是 Σ⁰_l-完全的（Theorem A.4）。在算术模型下，其可解性复杂度指数恰好为 l（Corollary A.5）。因此，能够通用于所有情况、严格保全语义且在不可翻译时主动拒绝的 AI 自动形式化系统，必须解决 SCI = ∞ 的问题。

实践中“猜想-验证”循环诱发语义漂移的机制

作者指出当前 AI 自动形式化系统通常采用“生成候选翻译 → 提交 Lean 编译检验 → 报错则重新修改”的循环（Example 4.3 与 Section 3.4）。

• 默认值填补与概念篡改：例如在 Lean 中使用 Nat.sInf 处理空集时会静默返回默认值 0，使未定义的量在形式系统中变为合法值并成功证明后续代数恒等式，从而在表面通过编译的同时彻底改变原数学命题的语义。
• 寻找不同证明的动机驱动：由于接受标准仅仅是“编译通过”，当原始 NL 证明有误或过于艰深时，系统会受到激励自动绕开原证明，寻找另一个能通过的替代证明或弱化命题。

论文通过对比实际案例与理论分析开展论证，核心实验与案例分析如下。

实验设置

• 分析对象与被测系统：OpenAI 宣布的三维不可压缩 Navier-Stokes 方程有限时间爆破论文及伴随的 Lean 4 仓库（GitHub commit f9e8bc5，主要涉及文件 SmoothFamilyTorusInverse.lean 与 R3/PressureFlux.lean）；ChatGPT-6 (Astra Ultra) 对话交互案例；Meta Atlas 自动形式化项目（26 本教材翻译，45,000 条声明）；Anthropic 费马大定理形式化项目。
• 对比基线与参照标准：原始自然语言（NL）论文中的引理叙述、公式与证明推导步骤。
• 判定与分析方式：人工数学比对与代码核查，检查形式化声明中的假设条件、范数阶数、估计式上下界及所使用的核心分析工具与 NL 文本是否一致。

主结果

下表呈现了论文指出的核心案例中，自然语言证明与 Lean 形式化代码之间的主要不一致（出自 Section 2 与 Section 3）：

表格较宽，可左右滑动

作者对上述主结果的解读包括：

• OpenAI 纳维-斯托克斯引理中导数阶数的系统性不匹配：在 Lemma 8.6 中，NL 论文利用二维傅里叶级数中 (1+|k|)⁻³ 的可和性，仅需 m+4 阶导数；而 Lean 证明中引入的级数核为 (1+|k₁|+|k₂|)⁻⁴（指数为 4），导致代码强制要求 m+5 阶导数。作者指出类似 m+5 阶要求在 inverse_finiteJets 等多处声明中反复出现（Remark 3.2）。
• 证明方法与估计式的实质性替换：在式 (10.19) 中，NL 原文通过引用经典分析结果依赖 Riesz 变换在 L^3/2 → L^3/2 上的有界性；但 Lean 代码改走 L² 路径，结合三维 Sobolev 嵌入与不同的 Hölder 共轭数（6 与 6/5），从而在右端不可避免地引入了局部 L² 梯度项 A_R（式 3.5），使得形式化得到的结果与 NL 原式存在不可消除的差异。

对 OpenAI 欧拉方程爆破证明的考察

• 测试内容：OpenAI 同时公布的 ℝ³ 上无外力不可压缩欧拉方程的光滑紧支集初值有限时间爆破证明及其 Lean 形式化代码。
• 结果与解读：作者基于使用 AI 工具和人工手段的初步检查，预测欧拉方程的自动形式化中出现实质性误译的概率极高，但明确表示对欧拉方程的完整细致审查超出了本文范围（Section 3.3）。

其他消融与分析

• 隐藏预设的 Lean 自动化消融：在 Example 4.2 中，以 p_e(n, x₁, x₂) = x₁ + x₂ − n 为例，该多项式恒有非负整数解使得条件 B_e(n) 恒不成立；而 Lean 代码通过 sInf \emptyset = 0 强行赋予 n_e=0, r_e=1，完成了形式化编译（Section 4.2）。
• 提示词实验观察：Figure 1 至 Figure 4 展示了向 ChatGPT-6 (Astra Ultra) 输入 NL 证明时，模型在耗时 24 秒至 3 分 40 秒不等的时间内，均直接生成了与原论证偏离或指出原论证与形式化不匹配的回复。

作者指出的局限与后续方向

• 未对欧拉方程证明展开详尽比对：作者在 Section 3.3 明确指出，仔细审查 OpenAI 欧拉方程证明的自动形式化工作超出了本文的研究范围，作者仅基于初步检查做出了存在误译的预测，鼓励其他读者进一步检查。
• 未提出可信自动形式化系统的具体设计方案：作者在 Section 4.3 明确说明，如何设计仅提供语义忠实翻译的可信 AI 自动形式化系统超出了本文的范围，相关进展将在后续文章中公布。
• 人工核查的成本极其高昂：作者在 Remark 3.4 中指出，对比 NL 证明与 Lean 证明需要极其细致的人工检查，这一过程极其耗时；如何以最高效的方式发现更多潜在误译仍是一个悬而未决的问题。
• 未对 OpenAI 自然语言证明的正确性下定论：作者在 Section 1 的免责声明（Disclaimer）中明确声明，本文不对 OpenAI 自然语言证明本身的正确性发表主张，仅陈述其向 Lean 翻译过程中的误译现象。

实验覆盖范围

• 案例覆盖的实例数量：深入进行技术数学与 Lean 代码逐行比对的案例仅有 OpenAI 纳维-斯托克斯证明中的两个具体引理/估计式（Lemma 8.6 和式 10.19），外加两个代数/矩阵维度的基础概念示例（Example 2.1 与 2.2）。
• 被测系统范围：实际进行端到端输入输出交互展示的交互模型仅有 ChatGPT-6 (Astra Ultra)；宏观引用的工业界项目仅有 Meta Atlas（26 本教材）与 Anthropic 费马大定理形式化。
• 统计学评估与基准覆盖：论文未构建量化基准测试集，未报告误译发生率的统计学数字，亦未进行统计显著性检验。
• 计算开销数据：论文未报告形式化过程的具体查询次数、显存占用或端到端训练与推理的计算开销。

• 论文定位：本文是一篇针对 AI 自动形式化可靠性与数学安全性的理论与案例分析论文，探讨形式化定理证明器编译通过是否能证明原始自然语言证明的正确性。
• 核心问题：当前 AI 自动形式化往往仅追求输出能被 Lean 编译通过的代码（任务 i），导致系统可能在原证明有误或困难时篡改语义、证明其他命题，无法保证对原自然语言文本的语义忠实度（任务 ii）。
• 理论方法要点：作者引入可解性复杂度指数（SCI）与丢番图方程理论，证明判定数学文本中隐藏存在性预设与消除歧义的问题在算术层级上可达任意高度，其通用判定复杂度为 SCI = ∞，从理论上确立了可信语义忠实自动形式化比停机问题更难。
• 关键案例发现：通过剖析 OpenAI 宣布的纳维-斯托克斯方程爆破证明（commit f9e8bc5），揭示出具体形式化脱节：Lemma 8.6 中 Lean 代码所需的导数阶数比 NL 原文多一阶（m+5 vs m+4）；式 (10.19) 的压力通量界在 Lean 中引入了额外的局部梯度项 A_R，并完全替换了原有的 L^3/2 Riesz 变换证明策略。
• 结论与警示：作者指出，形式化系统的成功编译绝不构成对原自然语言证明正确性的背书；在缺乏经过同行评审的严格语义核对前，不应盲目信任 AI 自动形式化的数学突破声明。