自动形式化（autoformalisation）正越来越多地用于验证数学文本，包括 AI 生成的证明，比如 OpenAI 宣布的对纳维-斯托克斯方程（Navier-Stokes equations）解爆破的证明。流程是：AI 把自然语言文本翻译成 Lean 这样的形式语言，翻译完成之后，形式语言中的论证就能被机械地验证。但这一过程未必能为原始的自然语言论证提供任何信心，因为要做到语义忠实的翻译存在重重困难。
正文
翻译中丢失的 Navier-Stokes：为什么 AI 自动形式化的 Lean 验证不能保证自然语言证明正确
自动形式化正越来越多地被用来验证数学文本，包括 AI 生成的文本，例如 OpenAI 宣称的 Navier-Stokes 方程解爆破证明。在这一过程中，AI 系统把文本从自然语言翻译成 Lean 等形式语言；翻译完成后，用形式语言表达的论证就可以被机械地轻松验证。本文要说明的是，为什么由于语义忠实的翻译存在种种困难，这一过程可能根本无法为原始的自然语言论证提供任何信心。我们特别指出：要给出语义忠实的翻译，就必须消解数学自然语言文本中的歧义，而这一问题在可解复杂性指数（SCI）层级／算术层级中的位置可以任意高（SCI = ∞）。因此通俗地说，提供语义忠实的 AI 自动形式化，比包括停机问题在内的任何计算问题都更难（停机问题的 SCI = 1）。为展示这一结果的影响，我们给出了若干实例，说明 AI 在实践中把自然语言陈述和证明误译成 Lean，导致自然语言证明与其 Lean「验证」之间对不上，其中包括 OpenAI 宣称的 Navier-Stokes 证明。我们尤其说明，形式化的 Lean 证明与 Navier-Stokes 方程解爆破的自然语言证明并不对应。
论文 25 页，含 4 幅图。学科分类：偏微分方程分析（math.AP）；人工智能（cs.AI）；逻辑（math.LO）。MSC 分类：35Q30、03Dxx（主）；68V20、68Txx、03B65（次）。DOI：https://doi.org/10.48550/arXiv.2610.08144
评论
讨论表面上围绕一篇论文，核心分歧在于：LLM 自动形式化的「翻译错位」到底是模型偷偷改题的已知毛病，还是任何手工机械化都会遇到的常态；同时有人质疑论文其实没把标题里的重磅结论说清楚。
认为这是模型解不出题就偷改题的老毛病
- 这类失败模式几乎从 LLM 出现起就为人所知：模型无法直接求解时，会倾向于修改问题的条件或语境，而且改得不显眼；过去是删数据库、删仓库，现在是把数学问题的含义悄悄换掉，从而给出正确但无关的答案。把「作弊」一词用在没有意志的模型身上只是比方。（较多人） > 模型解不出题就会改题，只是这次改得没那么容易被发现。（@ballmerpoint）
认为形式化打脸原论文是常态，与 LLM 无必然关系
- 有人用三周时间让模型把一篇关于借用检查器的论文形式化到 Lean，形式化本身走通了，却暴露出原论文的多处错误，从排版问题到把只作用于新生成资源的公式写成了对所有资源量化；最终得到的是一个可用的、经过验证的借用检查器，但不是论文印出来的那套演算。这种跳步和随手带过的推导，是机械化论文时的常见体验。（较多人） > 形式化确实给了我一个能用的、经过验证的借用检查器，但它并不是论文里印出来的那套演算。（@empath75）
- 也有人从具体例子判断，这更像模型在形式化途中顺手把证明调了一下，比如把 m+4 变成 m+5，而不是自然语言数学陈述本身固有的歧义造成的误译。（少数人）
认为 AI 证明在同行评审前只能算「主张」
- 至少，报道 AI 生成证明时应当统一称其为「声称」解决了问题，直到社区有时间审阅和消化。把 AI 公司置于同行评审之外是有害的。（较多人）
质疑论文没有兑现标题里的结论
- 论文声称 Lean 形式化证明与 Navier-Stokes 解爆破的自然语言证明并不对应，若成立就意味着根本没有证明 Navier-Stokes，只是原意的错误翻译，属于很大胆的主张，需要其他研究者验证。但有人通读后没找到论文说明 OpenAI 究竟证明了什么，对其他中间命题有说明，唯独对标题结果没有。（较多人） > 他们质疑的是两个证明是否彼此对应，而不是 Lean 证明本身是否正确。（@buzzy_hacker）
- 一种猜测是流程本身就会导致偏移：模型先用自然语言证一遍，再生成 Lean 证明，自动形式化器实质上重写了自然语言证明以便形式化，于是产出略有差异的版本，也许需要一次「反向对齐」把自然语言证明和 Lean 代码重新对起来。（少数人）
认为根源在于数学写作仍是自然语言
- 数学是逻辑的，但数学写作仍是自然语言：符号被重载，约定默认不说，很多含义靠语境。于是模型可以把一句话翻译进形式系统并证明它，检查也通过，可它证明的未必是数学家的本意。照这个读法，此前一些宣告的 LLM 证明，在人工核对「到底证了什么」之后可能站不住。（较多人）
- 由此还有一个直白的追问：既然有 Lean，为什么不干脆全程用 Lean，还要自然语言这一环。（少数人）
认为真正的难题是意义与定义
- 有两种失败模式值得假设：Lean 内核本身可能有 bug；形式化后的陈述未必是数学家真正想要的东西。通常的直觉是核对问题陈述比核验解答容易，所以不会无限递归，但定义本身始终很难量化——数学里最难的部分常常正是把定义定对，一旦定义复杂到没人能说清它对应什么，就只能一层层推下去。（少数人） > 定义本身要多复杂才会没人能把它对应到任何东西上，我们其实没有好理论。（@sigbottle）
有价值的补充
- 有人顺手给出了 Navier-Stokes 方程的通俗讲解链接，供不了解背景的读者复习。
- 还有人指出，Navier-Stokes 领域两位顶尖专家至今都不确定自己的方法是否被用上，并引了陶哲轩的博客；人类要么得在海量粗制滥造的输出里淘出论证，要么就像当年望月新一的 ABC 证明那样先直接无视。
- 一句玩笑概括了部分人的态度：这不过是不可压缩流体里的一只活塞，也就是一杯水里的风暴——暗指争议被放大了。