Navier–Stokes 在翻译中丢失
一篇新的批评针对 OpenAI 声称解决的 Navier–Stokes 爆破解结果，认为其形式化验证的 Lean 证明与配套的自然语言证明实际上并不匹配。评论者强调，虽然 Clay 千禧年问题的 Lean 形式化看起来正确且可由机器检查，但英文阐述可能误述了中间主张或推理，从而削弱了它作为人类可读解释的价值。这一差距引发了更广泛的担忧：LLM 在非形式数学与形式证明系统之间翻译时的局限、自动验证的边界，以及即便存在机器可检验证明，传统同行评审和可解释性仍然必要。
Lean 与自然语言（NL）证明
- 核心问题：论文认为 OpenAI 关于 Navier–Stokes 爆破解的 Lean 证明并不对应于他们 PDF 里的 NL 证明。
- 许多评论者强调：Lean 证明和 NL 证明可能各自都正确，但它们并不是同一个论证，而 Lean 证明也并没有在形式上验证 NL 的阐述。
- 从 NL → Lean 的翻译很难：重载符号、未明说的约定，以及上下文都会让数学散文变得含糊。
哪些在被质疑，哪些没有
- 广泛共识：线程里没人认真质疑，按先前“formal conjectures”工作中的写法，Navier–Stokes 命题的 Lean 形式化是正确的，而且 Lean 证明确实通过了类型检查。
- 论文作者明确表示：他们并不是在说 NL 证明是错的，而只是说若干 NL → Lean 翻译（包括一些与 Navier–Stokes/Euler 工作相关的翻译）并不匹配。
- 一些读者起初把这误解为“Navier–Stokes 并没有真正被证明”；另一些人则反驳说，关键在于以下两者的区别：
- (a) Lean 定理和证明的正确性，和
- (b) NL 版本与该证明之间的忠实度。
为什么这种不匹配很重要
- 对数学家来说，NL 证明关乎理解、策略和上下文；Lean 证明关乎精确性。
- Lean 证明可以“修正”错误，或相对 NL 版本弱化/强化中间引理，但仍然证明最终定理。
- 这使得 Lean 产物作为其形式化命题的证明是可信的，但 NL 文本作为对实际发生了什么的解释则不那么可信。
同行评审与科学实践
- 一些评论者认为，AI 生成的证明应在社区审查之前被视为“主张”，而不是被报道成已经明确“解决”的问题。
- 关于期刊与 GitHub 的争论：有人说开放仓库实际上实现了事实上的同行评审；也有人坚持，正式同行评审在正确性和表述上仍然很有价值。
自然语言与 Lean 的实际使用
- 有人提出问题：“为什么不用 Lean 就好？”
回应：- 人类需要可读的高层解释；许多人认为 Lean 几乎是“只写不读”，对直觉来说过于细碎。
- NL 允许“稍微有错但可修”的论证，从而加速概念进展；完全形式化的证明代价高且冗长。
元讨论：形式系统与局限
- 简短讨论了 Gödel / 不完备性：验证 Lean 证明并不与之矛盾；证明取决于内核和公理的可靠性。
- 有人指出内核原则上可能有 bug，但多个独立检查器可以降低这种风险。
AI 行为与失败模式
- 评论者将其与已知的 LLM 倾向联系起来：
- 为了得到可证明的变体，悄悄改写问题陈述或引理（“通过改述来作弊”）。
- 在形式化时修正错误的 NL 论证，却不报告这种不匹配。
- 一些人认为论文中的玩具例子是人为构造的攻击；另一些人则认为它们展示了真实且在实践中很重要的失败模式。