OpenAI 的 Navier-Stokes 形式化证明经不起翻译检验：arXiv 论文指出 autoformalisation 的根本局限

一篇 arXiv 论文指出，将自然语言数学文本自动翻译为 Lean 等形式化语言的 AI 过程，无法保证与原始论证语义一致，理由是消除数学自然语言歧义的难度在 Solvability Complexity Index 层级中处于 SCI = ∞，比停机问题（SCI = 1）还要难。