OpenAI 让一万个智能体跑 88 小时：交出千禧年难题之一的形式化证明
OpenAI 于 9 月 8 日发布《On the Navier–Stokes Millennium Prize Problem》，给出纳维–斯托克斯存在性与光滑性问题的证明（165 页），以及可在 Lean 中逐步机器校验的形式化，声称建立了 Fefferman 提法中的 (C)(D) 两条替代结论。执行者是约 1 万个并发智能体，9 月 1 日启动、9 月 5 日得出结论，约 88 小时，期间交换约 270 万条消息、消耗约 1300 亿输出 token，OpenAI 研究员 Bubeck 估计电费在数百万美元量级。所用模型未公开，公司称其能力显著强于 GPT-6 Astra，训练始于 8 月 28 日。OpenAI 表示不会申领 Clay 研究所的 100 万美元奖金。
意义有两层。第一层是能力：这是千禧年难题第一次拿到 AI 生成、且带机器可校验形式化的候选证明——即便最终被判定有漏洞，「几天时间、几百万美元、一次万人智能体协同」这件事本身已经把数学攻关的成本结构改了。第二层是它暴露的争议：纽约大学教授 Tristan Buckmaster 与 Anthropic 研究员 Levent Alpöge 在此前约 12 小时公布了相关的强迫欧拉方程结果，Buckmaster 公开指控 OpenAI 通过 Codex 会话接触到了他们的进展，并称在合署方案中被要求把 Alpöge 从作者名单剔除；OpenAI 否认获取私人研究数据，承认「去标识化、派生自使用」的数据可能进了训练。优先权与证明有效性都还在等独立数学家逐行评审，Clay 研究所尚未受理。