OpenAI宣布攻克千禧年难题 OpenAI 宣称内部模型解决了纳维-斯托克斯存在性与光滑性这一千禧年难题，却明确表示不申领一百万美元奖金。克雷研究所官网到 9 月 9 日仍把这个问题列为未解决。

这中间的距离值得说清楚。OpenAI 给出了分析证明，并用 Lean 做了形式化验证。Lean 验证保证的是代码层面的逻辑严密，机器跑通了这套证明。它不等于数学界承认结论成立。按克雷研究所的规则，证明要在公认期刊发表，再经过至少两年的社区审查，才可能被正式认定。

证明本身也还有未结的环节。结论属于官方问题陈述中的 C、D 情形，仍待同行评议。宣布攻克和真正被认定是两件事，这一段距离得由数学界用两年时间走完。