为什么 AI 自动形式化的 Lean 验证不能保证证明正确？

Lean 编译通过不等于语义保真

这里的自动形式化，指 AI 系统把数学文本从自然语言翻译成 Lean 等形式语言，之后形式论证可以被机器检查。论文区分了两件容易被混为一谈的任务。第一项任务只要求 AI 针对一份所谓的自然语言证明，产出能编译的 Lean 代码，且不使用 `sorry` 关键字或额外公理。第二项任务要求对每个定义、陈述和证明都做语义忠实的翻译，保留原文的数学内容以及结果之间的依赖关系。

论文的核心警告是：第一项任务成功，完全不能说明第二项任务成功。Lean 接受一份翻译，并不意味着语义被保留，因为许多候选翻译都能编译，其中一些忠实、许多并不忠实。因此，如果 AI 选择了误译，Lean 不会提供任何安全网；形式证明正确，也不能说明自然语言证明正确。

作者明确界定了这一主张的范围：他们并未断言 OpenAI 的自然语言 Navier-Stokes 证明是错的。他们讨论的是翻译成 Lean 时的误译，以及 Lean 验证能证明什么、不能证明什么。

消解歧义的问题位于无界 SCI

要做到忠实翻译，AI 必须消解数学自然语言文本中的歧义，包括某个被定义的对象是否真的存在。论文把这一问题形式化为预设消解问题，并将其放入可解复杂度指标（SCI）层级，该层级推广了算术层级。结论是：消解歧义这一问题的 SCI 等于无穷大。

作者给出的对比很鲜明：停机问题的 SCI 等于 1，所以语义忠实的自动形式化在非正式意义上比任何计算问题都更难，这里的“任何计算问题”指任何具有有限 SCI 的问题。论文把这一点精确表述为对可信自动形式化器的要求：一个总是输出语义忠实翻译、或声明该陈述无法翻译的系统，必须解决比任何有限 SCI 问题都更难的问题。

证明建立在最小数构造之上，这类构造是否有良好定义，取决于某个自然数集合是否为空。推论 A.5 表明，对每个不小于 2 的层级 l，相应的判定问题 SCI 恰好为 l，因此对所有层级回答该问题的问题，其 SCI 等于无穷大。这是关于翻译任务难度的结论，而不是对当前模型出错频率的测量。

错误的自然语言证明也能在 Lean 中编译

论文最简单的演示用一个多项式不等式。自然语言证明声称 p(x) = x^3 - x^2 - x + 1 的根为 -1（二重）和 1（一重），并由此得出当 x 不小于 -1 时 p(x) 非负。所声称的重数是错的，因此给出的因式分解也是错的。

当用户要求聊天机器人把这段论证写成能编译的 Lean 证明时，机器人通过找出正确的重数，返回了一份正确的 Lean 证明。形式证明有效，但它并不是对用户所给论证的翻译。这是最清楚的不匹配情形：自然语言证明错误，Lean 证明正确，而编译结果对原始论证什么也说明不了。

第二个例子展示了同样的缺口，但其中没有错误。对于实对称矩阵 A，自然语言证明在正交归一特征基下对角化 A，并把 A 平方的迹化为特征值平方和。Lean 证明则保留原矩阵，利用对称性得到元素平方和。两个证明都正确，但 Lean 论证与用户要求形式化的那个论证明显不同。

OpenAI 的 Lean 估计多需要一个导数

论文最具体的技术比较针对 OpenAI 公布的 Navier-Stokes 爆破证明中引理 8.6 的方程 (8.19)。在自然语言论文中，这个逆估计用 F 的 C^{m+4} 范数乘以一个常数来界定 N^{-1}F 的 C^m 范数。在被引用的 Lean 声明中，相应的界需要 F 的 C^{m+5} 范数。

多出的这个导数不是表面差异。自然语言证明在二维情形下使用了项为 (1+|k|)^{-3} 量级的收敛级数，这正是多四个导数所换来的。Lean 代码则调用了一个系数半范数界，产生项为 (1+|k1|+|k2|)^{-4} 量级的级数，因此需要多五个导数。论文指出，其他 Lean 声明中也出现类似的 m+5 要求，包括 `inverse_finiteJets` 和 `mixedJet_inverse_bound`。

由于 Lean 估计严格弱于自然语言估计，这一形式化并没有确立自然语言论文所陈述的命题。论文还指出，有些 Lean 结果与自然语言中的界不可比较，因为导数类型不同，例如 Lean 定理使用混合导数，而不只是环面导数。

压力通量界同时改变了陈述与论证

第二项比较针对自然语言论文的方程 (10.19)，这是一个用于速度唯一性引理证明内部的压力通量估计。自然语言中的界只用 B_R（一个局部化的 L^6 速度范数）表述。Lean 估计还额外依赖 A_R（一个局部化的 L^2 梯度范数），因此两个界很难直接比较。

论文把这一分歧追溯到三处证明方法的改变。Lean 证明没有依赖 Riesz 变换作为 L^{3/2} 到 L^{3/2} 映射的有界性，而是调用 Sobolev 嵌入转到 L^2，并在那里使用 Riesz 有界性；正是这一嵌入带来的额外导数，使 A_R 出现。Lean 证明还以不同的指数应用 Hölder 不等式，改变了最终的界；它同时显式证明左侧积分关于时间连续，从而把几乎处处成立的陈述升级为不带该限定词的陈述。

论文还记录了一处积分拆分方式的结构差异：自然语言证明用一个含 φ_R^3 的测试函数分解被积函数，而 Lean 证明用 φ_R^2 和一个含 φ_R^5 的测试函数来拆分。作者指出，自然语言中的界实际上更严格，因为该引理的目的是证明 w 为零，但这一点要在引理 10.5 的整个证明完成之后才能确立。

Lean 检查能证明什么、不能证明什么

论文的实践结论来自两类自动形式化任务的区分。如果目标是判断一个自然语言论证是否正确，那么相关的任务是语义忠实的翻译，而论文证明的正是这项任务具有无界 SCI。对 AI 翻译做 Lean 编译，处理的是更容易的那项任务：AI 可以自由地产出所陈述定理的任意一份能编译的证明。

因此作者主张，OpenAI 的自然语言证明以及其他经过自动形式化的 Lean 证明，不应在未经与其他证明同等同行评审和审视的情况下被直接信任。Lean 代码告诉我们定理是正确的，但自然语言证明及其中间论证、引理和结果可能不正确，或者包含错误的论证。

论文并未声称展示了如何构建可信的自动形式化器；它明确表示这超出本文范围，是一个重大开放问题。它确实声称，即便是 OpenAI 最先进的模型也远未达到语义保真。这一主张的具体证据是本文记录的这些误译，而不是对模型准确率的系统性基准测试。

不匹配最要紧的地方

本文中的各项比较并不属于同一类型，这一差异决定了每项比较能承载多大分量。多项式与矩阵的例子表明，一份能编译的 Lean 证明可能与所提供的自然语言论证毫无关系，包括该论证本身错误的情形。Navier-Stokes 的比较则更进一步：在导数估计中，Lean 陈述严格弱于自然语言陈述；在压力通量情形中，界和用来确立它的数学论证都不同。

这一排序是论文对评估自动形式化数学的读者最有用的要点。Lean 检查作为关于它实际编码的形式陈述的证据最强，而作为关于本应被翻译的自然语言证明的证据最弱。当形式陈述偏离自然语言陈述时，这一缺口就会扩大，无论偏离来自多一个导数、多出对 A_R 的依赖，还是来自不同的证明策略。

因此论文自身的优先项是忠实翻译任务，而不是编译证明任务。其无界 SCI 结果解释了为什么这一优先项无法仅靠更好的工程解决，而其 Navier-Stokes 例子展示了失败在一个高关注度案例中的样子：形式化可以有效，而它本应认证的自然语言论证仍未得到验证。

本文引用的文献