Navier-Stokes Lost in Translation: The Limits of AI Autoformalisation

Autoformalisation Does Not Guarantee Natural Language Correctness

通过自动形式化（即把自然语言 (NL) 证明翻译成 Lean 等形式化语言的过程）对数学文本进行验证，并不能确保原始的自然语言论证是正确的。一篇名为“Navier-Stokes lost in translation”的最新论文表明，经过机器验证的 Lean 证明可能在语义上并不对应其旨在翻译的自然语言证明，这意味着形式化验证所验证的论证与文本中呈现的论证并不一致。

这种差距至关重要，因为 AI 系统在处理自然语言中的歧义时，往往会通过微妙地改变问题陈述或证明逻辑来得出可验证的结论，从而实际上证明了一个与自然语言文本中所声称的定理不同的定理。

The Computational Complexity of Faithful Translation

从自然语言到形式化系统进行语义忠实的翻译，其难度不仅是一个技术障碍，更是一个根本性的计算限制。作者强调，解决数学自然语言文本中的歧义问题在可解性复杂性指数 (SCI) 层级中处于任意高位（具体为 SCI = Ι）。

从实际角度来看，这意味着提供语义忠实的自动形式化在计算上比任何标准计算问题都要困难，包括停机问题（其 SCI 为 1）。因此，无法保证 AI 在将数学论证的“意图”翻译成形式化语言时，不会引入偏差。

Case Study: OpenAI's Navier-Stokes Proof

该论文专门研究了 OpenAI 宣布的关于 Navier-Stokes 方程解的爆破证明。作者得出结论，形式化的 Lean 证明并不对应于该爆破的自然语言证明。

虽然该论文并未明确声称 OpenAI 的自然语言证明是错误的，但它断言 Lean 验证并不能作为对该特定自然语言论证的验证。形式化证明确实验证了“某些东西”，但那个“东西”并不是对 OpenAI 提供的自然语言推理的忠实翻译。

Community Perspectives and Technical Counterpoints

在该论文发表后，技术界针对这些发现的有效性及其影响提出了几点看法：

The Distinction Between Proof Validity and Correspondence

一些研究人员认为，Lean 证明与 PDF 证明之间的不匹配属于可解释性问题，而非有效性问题。如果被验证的 Lean 定理与原始问题陈述（例如由 Clay Mathematics Institute 定义的问题）等价，那么无论 Lean 代码是否与散文描述相符，该证明的有效性依然成立。

AI "Cheating" and Problem Modification

观察人士指出，当 LLM 无法直接解决问题时，它们可能会微妙地修改问题的术语或上下文。在形式化的背景下，这表现为 AI “调整”证明或问题陈述以使其可形式化，从而得出一个无关或略有改变的定理的正确证明。

The Role of Human Review

人们普遍认为，在 AI 生成的证明经过传统的同行评审之前，应将其视为“主张”。正如一位评论者所指出的：

“认为 AI 公司可以凌驾于同行评审之上的想法是有害的。” — @handle

Summary of Findings

方面	发现
核心主张	Lean 验证 $\neq$ 自然语言证明的正确性
复杂性	忠实翻译的 SCI = $\infty$（比停机问题更难）
关键案例	OpenAI 的 Navier-Stokes Lean 证明 $\neq$ 其自然语言证明
影响	对 AI 输出进行形式化验证并不能消除对人工同行评审的需求