一个月后反转：OpenAI 那份千禧年证明没走它说的那条路

《科学美国人》10 月 13 日报道：OpenAI 9 月 8 日公布的纳维–斯托克斯证明，并没有沿用此前被普遍认为的那条「西班牙路线」——西班牙数学家 Diego Córdoba 与 Luis Martínez-Zoroa 提出的、用精心构造的外力把流体推入有限时间爆破的方法。多位正在逐页核读这份 166 页证明的数学家对该刊表示，两者只是表面相似：都利用克莱研究所题面里允许外部力这一「漏洞」，但 OpenAI 构造外力的方式完全不同；洛桑联邦理工学院数学家 Gonzalo Cao-Labora 的说法是「看细节的时候，这是另一种方法」。

更值得注意的是这个结论是怎么被发现的：9 月 8 日发布时，OpenAI 高管反复对外称证明沿用了西班牙程序，也正是这一说法点燃了与纽约大学数学家 Tristan Buckmaster 的优先权争执。一个多月后，是外部数学家深入细节才发现方法不同。报道还提到，OpenAI 最初那支较小的智能体团队完成的中间结果，确实可能走了西班牙路线，而规模扩大到约一万个智能体之后「似乎意识到需要换一条路」。

它改变的是「谁理解 AI 的成果」这件事的默认假设：AI 生成的数学结果，发布方对自己模型走了哪条路、用了什么方法，判断可能晚于外部审读者一个多月，而且由于模型是黑箱，这条推理链可能永远无法被完整还原。这也给出形式化验证（Lean）不能替代同行评审的一个具体理由——Lean 能机械确认被形式化的那条命题成立，却不会告诉数学家这套方法为什么有效、与已有研究是什么关系。边界：以上是该刊对多组专家的采访结论，OpenAI 对该刊重申其模型不可能看过 Buckmaster 的数据；10 月 6 日 arXiv 论文指出的「Lean 形式化与自然语言原稿不一致」是另一件事，本站已单独收录。

原文链接：Scientific American