OpenAI 的纳维-斯托克斯证明被质疑

前阵子 OpenAI 拿出一份 166 页的纳维-斯托克斯问题潜在证明，当时不少人觉得这是 AI 攻克千禧年难题的信号。但最近几组专家复核后给出的结论是：它和西班牙数学家 Córdoba、Martínez-Zoroa 的路线只是表面相似，深入细节后其实是另一套东西。EPFL 的 Gonzalo Cao-Labora 直接用了「different approach」这个说法，这个措辞在数学圈已经算相当不留情面了。

我比较在意的是这份证明的呈现方式。它用 Lean 写成，每一步逻辑都能被机器校验，但机器校验通过不等于人类能读懂，也不等于思路原创。Clay 数学研究所从发布起就在审，到现在也没有给出定论，这本身就说明问题没那么简单。对做形式化验证的团队来说，Lean 是加分项；但对判断数学贡献来说，它反而把可读性这道门给关上了。另一个争议点是训练数据。NYU 的 Tristan Buckmaster 在发布前就指控 OpenAI 建立在本人和 Anthropic 的 Levent Alpöge 用公开模型所做工作的基础上，OpenAI 否认用过他的数据。IAS 的 Camillo De Lellis 说得挺实在：语言模型是黑箱，想给出确定答案基本不可能。我觉得这才是整件事最尴尬的地方——不是谁对谁错，而是这类争议在现有技术条件下根本没法裁决。十月初 OpenAI 又放出了大约 400 条后续结果，节奏明显是想用数量把讨论往前推。但数学共同体认的是可复现、可追溯的论证链，不是发布频率。如果每一份产出都要靠外部专家花几周去反推它到底站在谁的肩膀上，那这套协作模式本身就跑不通。我的判断是，AI 在形式化数学上确实在快速进步，Lean 生态也会因此受益。但把「机器验证通过」直接等同于「数学上的新贡献」，目前看还是太乐观了。