AI 不再只是聊天写代码，它第一次把"形式化数学证明"跑通了一条完整链路。对科学计算方向的人，这是一声发令枪：agent 已经能承担"发现 + 验证"的科研流程。
9 月 8 日，OpenAI 公布一项里程碑式研究。
其多智能体系统协作解决了与 Navier–Stokes 方程相关的千禧年难题的一个版本。
一次硬核的里程碑
过程相当硬核：近 100 个 agent 并行工作了约 50 小时。
它们先意外解出 Euler 方程（无外力情形）的正则性反例。
随后在 9 月 5 日给出 Navier–Stokes 某版本的解，再由 GPT-6 Astra 用 Lean 做形式化验证，耗时约 17 小时。
整轮研究发出 490 万条消息、消耗约 3000 亿输出 token。
这条链路说明，AI 已经能把"猜想—实验—证明"的环节串起来。
划清边界，别被标题党带偏
需要厘清它到底解了什么：OpenAI 明确"不主张千禧年大奖"。
称这是 AI 能力进展的"快照"而非终解，解出的是特定变体，并非完整的存在性/光滑性判定。
更难能可贵的是研究操守——OpenAI 得知同期有 Anthropic 员工与 NYU 教授也在攻关后，主动联系对方承认其优先性、提议联合发布。
它在 9 月 6 日完成 Lean 验证后才公开，并强调：人仍设定研究方向、判断结果、掌控节奏。
诚实的边界感，恰恰让这个结果更可信、也更值得参考。
对 AI 大数据工程师意味着什么
形式化验证 + 多智能体协作，已经能把"提出猜想→跑实验→形式化证明"的科研循环部分自动化。
这预示着科学计算、仿真、数值分析里那些"靠人海堆时间"的环节，未来可能交给 agent 流水线。
当然，模型能力越强也越难监控，OpenAI 在同期《研究加速》一文中已把"agent 加速研究"的测算公开。
它把安全审查前移到训练全生命周期——这本身也是从业者该关注的治理趋势。
图片来源：Pexels
来源：OpenAI 官方研究页《On the Navier–Stokes Millennium Prize Problem》