Lean 验证通过不代表自然语言证明正确：从 Navier-Stokes 看自动形式化局限

arXiv 论文 2610.08144 分析了自动形式化（autoformalisation）的可靠性问题，即用 AI 将自然语言数学文本翻译成 Lean 等形式语言再做机械验证的流程。作者指出，解决数学自然语言中的歧义在 Solvability Complexity Index 层级中位置为 SCI = ∞，高于任何可计算问题（停机问题仅为 SCI = 1）。论文给出多个 AI 将自然语言陈述误译入 Lean 的实例，导致自然语言证明与 Lean 验证不匹配。这些实例包括 OpenAI 公布的 Navier-Stokes 方程解爆破证明，作者论证其形式化 Lean 证明与原始自然语言证明并不对应。