新论文指出 OpenAI 纳维–斯托克斯结果的 Lean 证明与文字证明「对不上」：机器校验通过，不等于原论证被验证

论文说了什么

9 月，OpenAI 公开了纳维–斯托克斯方程爆破问题上的结果，并附上 Lean 形式化证明，本站当时报道过它证的并非千禧难题的经典版本。10 月 6 日，Alexander Bastounis、Fabian Circelli 和 Anders C. Hansen 在 arXiv 提交论文《Navier-Stokes lost in translation》，副标题直接点明主张：AI 自动形式化后的 Lean 校验，并不能保证自然语言证明是对的。

论文列举了多个 AI 把文字命题和证明翻译成 Lean 时的误译案例，OpenAI 的纳维–斯托克斯结果是其中之一：作者认为，形式化后的 Lean 证明与文字版的爆破证明并不对应。据 TechCrunch 报道，论文记录了至少两处这样的不一致。

它没有说什么

作者没有声称 OpenAI 的结果是错的。论文的结论更窄，也更根本：Lean 只检查它被告诉要证明的那个命题，如果翻译时命题就被改了，校验通过并不能说明原来的文字论证成立。作者还从计算复杂性的角度论证，消除数学文本中的歧义、做到忠实翻译，本身就极难完全自动化，因此 AI 自动形式化需要人去做语义层面的核对。

对那批数学稿件的提醒

这篇论文出现的时间点很巧：OpenAI 10 月 6 日刚公开一批由内部模型产出的数学稿件，并把部分 Lean 形式化当作可信度的依据。按 TechCrunch 的统计，其中约 42% 做了形式化；TechCrunch 还援引哈佛数学家 Melanie Wood 的话说，结果发布时还没有人真正理解它，「工作才刚开始」。

这给读者一个具体的判断方法：看到「已用 Lean 验证」时，要追问被验证的到底是哪个命题，它和论文里写的结论是否一字不差地对应。在有人做过这层核对之前，「机器已检查」和「结论已成立」之间仍隔着一步。