Navier-Stokes 在翻译中走失：为何 Lean 验证不能保证自然语言证明正确
来源：arxiv.org — 2026-10-06
📋 概述
论文指出，把自然语言数学文本自动形式化为 Lean 再机械验证，并不能保证原始论证正确，因为忠实翻译本身极难。作者证明，消解数学文本歧义的问题位于可解性复杂度层级中任意高的位置（SCI = ∞），也就比 SCI = 1 的停机问题更难；并以若干 AI 误译实例为证，包括 OpenAI 宣称的 Navier-Stokes 爆破证明——其 Lean 形式化与自然语言证明并不对应。
🔑 核心要点
- 自动形式化（AI 把自然语言译为 Lean）并不能保证原始自然语言论证正确
- 消解数学文本歧义的问题位于 SCI = ∞，比 SCI = 1 的停机问题还难
- 因此“语义忠实的自动形式化”比任何计算问题都更难
- 文中给出若干 AI 误译自然语言陈述与证明的实例
- 其中包括 OpenAI 宣称的 Navier-Stokes 爆破证明，其 Lean 证明与自然语言证明并不对应
💡 金句
提供语义忠实的 AI 自动形式化，比包括停机问题在内的任何计算问题都更难。
👍 0
👎 0
← 返回 Lobsters 首页