Hacker News· nill0·· 2 天前精选AI 评分56
arXiv 论文论证 AI 自动形式化难以忠实翻译，质疑 OpenAI Navier–Stokes 证明
Navier–Stokes Lost in Translation
AI 导读
arXiv 论文 2610.08144 论证，将自然语言数学文本语义忠实地翻译为 Lean 等形式语言在 Solvability Complexity Index 层级上达到 ∞，难度高于停机问题。论文给出多个 AI 将 NL 陈述与证明误译为 Lean 的实例，包括 OpenAI 此前宣布的 Navier–Stokes 方程 blow-up 证明，并指出其形式化版本与 NL 证明不对应。
推荐理由
论文给出形式化翻译的复杂度下界，并用 OpenAI Navier–Stokes 案例展示 NL 证明与 Lean 验证之间的不一致。
正文 · AI 翻译
摘要：自动形式化越来越多地用于验证数学文本，包括由 AI 生成的文本，例如 OpenAI 宣布的关于 Navier-Stokes 方程解的爆破性的证明。在此过程中，AI 系统将文本从自然语言（NL）翻译成形式语言，如 Lean。一旦完成翻译，形式语言中表达的论证就可以轻松地进行机械验证。本文的目的是论证为什么这一过程可能对原始 NL 论证没有信心，原因在于进行语义忠实的翻译存在各种困难。特别是，我们强调，为了提供语义忠实的翻译，解决数学 NL 文本中的歧义问题在可解性复杂度索引（SCI）层级/算术层级中是任意高的（SCI $= \infty$）。因此，非形式地说，提供语义忠实的 AI 自动形式化比任何计算问题都更难，包括停机问题（其 SCI $= 1$）。为了展示这一结果的效果，我们提供了 AI 在实际中将 NL 陈述和证明误译为 Lean 的若干例子，导致 NL 证明与其 Lean `验证'之间不匹配。这些例子包括 OpenAI 宣布的 Navier-Stokes 证明。特别是，我们表明形式化的 Lean 证明并不对应于 Navier-Stokes 方程解的爆破性的 NL 证明。
| 评论： | 25 页，4 图 |
| 主题： | 偏微分方程分析 (math.AP)；人工智能 (cs.AI)；逻辑 (math.LO) |
| MSC 分类号： | 35Q30, 03Dxx（主要）以及 68V20, 68Txx, 03B65（次要） |
| 引用为： | arXiv:2610.08144 [math.AP] |
| （或 arXiv:2610.08144v1 [math.AP] 为此版本） | |
| https://doi.org/10.48550/arXiv.2610.08144 arXiv 通过 DataCite 发布的 DOI（待注册） |
投稿历史
来自：Alexander Bastounis [查看邮件]
[v1]
2026 年 10 月 6 日 周二 10:58:01 UTC（1,080 KB）
来源：Hacker News · arxiv.org