OpenAI的Navier-Stokes证明为何失效
Navier–Stokes Lost in Translation
Autoformalisation正被广泛用于验证AI生成的数学文本，例如OpenAI宣称证明了Navier-Stokes方程解的爆破。然而，这一过程存在严重隐患：AI将自然语言翻译成Lean等形式语言时，难以保证语义忠实。文章指出，消除数学自然语言中的歧义，其难度在Solvability Complexity Index层级中达到无穷大，甚至超过了停机问题。这意味着，即使Lean验证通过，原始自然语言证明也可能完全错误。作者通过多个实例，包括OpenAI的Navier-Stokes证明，展示了AI翻译导致的Lean验证与自然语言证明不匹配的问题。
提供语义忠实的AI自动形式化，比任何计算问题（包括停机问题）都要困难。
HN 评论区
151- ComplexSystems
除了关于 AI 的常规争执外，真正的重磅炸弹似乎是这一点：
“特别是，我们证明了形式化的 Lean 证明并不对应于纳维 - 斯托克斯方程解爆破的自然语言（NL）证明。”
所以这些作者似乎是在声称 OpenAI 根本就没有真正证明纳维 - 斯托克斯方程。如果我理解对了他们的意思，他们是在说大语言模型（LLM）并没有正确地将原始的纳维 - 斯托克斯“自然语言”思想形式化。如果属实，这意味着他们所谓的 Lean 证明根本不是纳维 - 斯托克斯的证明，而只是对原始自然语言思想的一次错误翻译。如果这是正确的，那么这是一个非常大胆的声明，我很想看看其他研究人员是否同意。
- stared
想简单了解一下纳维 - 斯托克斯方程是什么，请看：https://p.migdal.pl/equations-explained-colorfully/#navier-s...
- buzzy_hacker
如果我理解正确的话，这是在质疑自然语言证明与 Lean 证明之间的等价性，而不是质疑 Lean 证明本身的正确性？
- vanyle
这篇论文基本上是大堆废话。首先，自然语言不如 Lean 精确，因此将自然语言论证翻译成 Lean 有多种方式。如图 1 所示，LLM 在简洁地翻译关于根的论证方面做得还不错。
此外，该论文声称纳维 - 斯托克斯的自然语言论证比 Lean 论证更强。我的理解是，翻译用的 LLM 偷懒了，只写了满足定理所需的最少代码，而没有包含那些额外的更强断言。
在数学论文中，说“顺便提一下，这实际上证明了 [更强的断言]