Skip to content

Translation in progress Some entries still include text in the original language.

Original
论文追踪· arXiv:2610.08144·Indexed by this site · Originally publishedSelectedAttention53

New paper says Lean verification cannot endorse OpenAI's Navier-Stokes natural language proof

Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

Quick read

Analysis and theory

Based on 论文 PDF （Gemini 生成）; refer to the original

论文分析指出 Lean 编译成功不保证自然语言数学证明无误，证明消除歧义具有无穷大 SCI，并揭示 OpenAI 纳维-斯托克斯形式化存在导数阶数不符。

Questions
自动形式化日益用于验证自然语言数学证明，但形式化系统（如 Lean）编译通过并不保证原自然语言证明正确，AI 可能生成语义不忠实的翻译或证明了不同命题。
Methods
区分两类自动形式化任务，指出仅以 Lean 编译通过为目标会导致语义失真；通过希尔伯特第十问题证明数学歧义消解在 SCI 层级上为无限大（比停机问题更难）；结合 OpenAI 纳维-斯托克斯方程等实际案例展示自然语言与形式化证明的脱节。
Experiments and results
在 OpenAI 纳维-斯托克斯方程形式化中指出两处具体不一致：Lemma 8.6 中自然语言需 m+4 阶导数而 Lean 形式化需 m+5 阶导数；式 (10.19) 中形式化引入了自然语言中没有的梯度项 AR，且证明策略存在实质差异。
Limitations and future work
局限与覆盖范围仅限于论文明确讨论的内容：论文未对欧拉方程的自动形式化进行类似纳维-斯托克斯方程的逐项细致人工比对；理论复杂度结果（SCI = ∞）建立在希尔伯特第十问题与预设消解的理论构造上；未提供量化基准测试或统计检验；未报告具体查询次数或耗时。
Experimental setupChatGPT-6 (Astra Ultra) · OpenAI Finite time blowup for Navier-Stokes (NL paper & Lean 4 repo)、Meta Atlas (26 mathematics textbooks) · 语义忠实度（Semantic Faithfulness）、导数阶数（Derivative order m+4 vs m+5） et al.
Evaluated models
ChatGPT-6 (Astra Ultra)
Benchmarks
OpenAI Finite time blowup for Navier-Stokes (NL paper & Lean 4 repo)Meta Atlas (26 mathematics textbooks)
Metrics
语义忠实度（Semantic Faithfulness）导数阶数（Derivative order m+4 vs m+5）可解性复杂度指数（SCIA）
AI summaryand selection rationaleResearchers from the University of Cambridge and King's College London published a paper arguing that automated formalization in AI cannot guarantee semantic fidelity, so Lean's formal verification of OpenAI's claimed proof of the blow-up of solutions to the Navier-Stokes equations cannot prove the correctness of the natural language proof. The authors point out that the difficulty required to resolve ambiguity in mathematical natural language is infinite in the Solvability Complexity Index (SCI) hierarchy, harder than the halting problem (SCI=1), and provide multiple instances where AI mistranslates natural language statements and proofs into Lean. In OpenAI's Navier-Stokes proof, the Lean formalization does not correspond to the natural language paper: the estimate in Lemma 8.6 of the paper uses derivatives of order m+4, while the corresponding Lean theorem norm_derivativeWord_inverse_le uses derivatives of order m+5, with a weaker conclusion; the bound and proof approach for the pressure flux estimate (10.19) also differ from the Lean version.

Researchers from the University of Cambridge and King's College London published a paper arguing that automated formalization in AI cannot guarantee semantic fidelity, so Lean's formal verification of OpenAI's claimed proof of the blow-up of solutions to the Navier-Stokes equations cannot prove the correctness of the natural language proof. The authors point out that the difficulty required to resolve ambiguity in mathematical natural language is infinite in the Solvability Complexity Index (SCI) hierarchy, harder than the halting problem (SCI=1), and provide multiple instances where AI mistranslates natural language statements and proofs into Lean. In OpenAI's Navier-Stokes proof, the Lean formalization does not correspond to the natural language paper: the estimate in Lemma 8.6 of the paper uses derivatives of order m+4, while the corresponding Lean theorem norm_derivativeWord_inverse_le uses derivatives of order m+5, with a weaker conclusion; the bound and proof approach for the pressure flux estimate (10.19) also differ from the Lean version.

Why it was selected论文用可解性复杂度层级论证语义忠实的自动形式化比停机问题更难，并给出 OpenAI Navier-Stokes 证明中 Lean 与自然语言不一致的具体例子。

Paper analysis

6 questions; open one to read the full answer

  1. What problem does this paper attempt to solve?

    形式语言编译通过不等于自然语言证明正确，语义忠实消歧在理论上比停机问题更难。

    这篇论文试图解决的核心问题是：为什么通过 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 自动形式化在实践中发生的严重语义误译与证明脱节。

  2. What related research exists?

    梳理了语义哲学、SCI 复杂度与丢番图方程理论，并评述了近期工业界的大规模形式化实践。

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

    • 自然语言与形式语言的语义理论：论文追溯了逻辑学、语言学与哲学界关于自然语言到形式语言转换及语义保持的长期讨论，引用了 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 的爆破证明给出了具体的形式化脱节证据。

  3. How does the paper address this problem?

    建立两类形式化任务区分，证明语义忠实消歧为 SCI=∞ 难题，揭示编译反馈循环导致的语义漂移。

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

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

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

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

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

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

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

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

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

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

  4. What experiments did the paper conduct?

    通过 OpenAI 纳维-斯托克斯证明、ChatGPT-6 交互及 Meta 实践，揭示了阶数不符与证明替换等实际脱节。

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

    实验设置

    • 分析对象与被测系统：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）：

    Swipe horizontally to read the table

    案例来源自然语言（NL）表述 / 证明Lean 形式化代码 / 输出结果性质与脱节形式（出处）
    多项式根非负性（Example 2.1）声称根为 -1（重数 2）与 1（重数 1），因式分解错误纠正重数并给出完全正确的因式分解证明NL 证明错误，但形式化给出了正确的全新证明（Figure 1）
    实对称矩阵迹（Example 2.2）采用标准正交基对角化，利用迹的基变换不变性证明省略对角化与基变换，直接展开并利用矩阵对称性证明NL 与 Lean 证明均正确，但数学论证路径完全不同（Figure 2）
    OpenAI NS 逆估计（Example 3.1）Lemma 8.6, 式 (8.19)：|N−1F|Cmy ≤ Cm |F|Cm+4ynorm_derivativeWord_inverse_le：要求 m+5 阶导数有界Lean 证明的是严格弱于 NL 声明的结果，导数要求高出一阶（Figure 3）
    OpenAI NS 压力通量界（Example 3.3）式 (10.19)：上界纯粹由 BR 表示，依赖 L3/2 Riesz 有界性exists_uniform_actual_pressure_flux_bound：引入 AR 依赖且指数改变形式化改变了界的形式，且替换了原 Sobolev 嵌入与 Riesz 分析路径（Figure 4）
    Meta 教材形式化（Section 5.1）论文声称形式化了某教材 56% 的目标命题，代数几何约 60%Lean 社区核查指出原书声明 0% 准确形式化，其余仅覆盖 Mathlib 既有内容自动化形式化发生大规模语义误译与虚假形式化（Section 5.1）

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

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

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

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

    其他消融与分析

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

  5. What are some points that can be further explored?

    作者指出未详审欧拉方程且设计可信系统超范围；实验仅深入剖析少数案例且未提供统计基准。

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

    • 未对欧拉方程证明展开详尽比对：作者在 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 费马大定理形式化。
    • 统计学评估与基准覆盖：论文未构建量化基准测试集，未报告误译发生率的统计学数字，亦未进行统计显著性检验。
    • 计算开销数据：论文未报告形式化过程的具体查询次数、显存占用或端到端训练与推理的计算开销。

  6. Summarize the main content of the paper

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