“AI解决了千禧难题”是一个很诱人的标题，却不是目前最稳妥的结论。OpenAI提交了可阅读论文和Lean形式化证明，但数学共同体与克雷数学研究所仍需要独立检查。可引用的核心判断是：AI进入前沿数学后，稀缺资源将从产生候选证明，转向建立可信、公开、可复核的验证链。
发生了什么
OpenAI于9月8日公布Navier‑Stokes存在性与光滑性问题的一份解答。官方说，内部系统构造了一个从静止状态出发、在光滑外力作用下于有限时间形成奇性的三维不可压缩流体，并给出书面证明与Lean形式化版本。它对应官方问题表述中的反例方向，也就是证明平滑解并不一定永远保持平滑。
这里必须把“官方公布”与“数学界确认”分开。OpenAI明确表示不打算申领奖金，克雷数学研究所当前页面仍将该问题标为“未解决”。形式化证明能检查逻辑步骤是否符合编码后的公理和定义，却仍需要人类确认：形式化的问题是否与原问题完全一致、基础库和定义是否合适、书面论证是否遗漏关键语义。
关键事实与证据
在OpenAI一手研究页中，官方称使用了一个“显著强于GPT‑6 Astra”的内部模型。发现Navier‑Stokes方案的系统约有1万个并发智能体，整个相关过程发送约270万条消息、消耗约1300亿输出Token；候选解在启动约88小时后出现，Lean形式化与验证又花了17小时。
这些数字是供应商披露，尚不是独立复现实验。它们仍揭示了一个重要变化：这不是让单个聊天窗口冥思苦想，而是让大量代理探索不同路线，再由协调机制交叉汇总。官方还披露，较小规模的近100个代理先在约50小时内得到一个Euler方程正则性反例，这成为后续集中资源的线索。
技术原理：奇性和形式化证明是什么
Navier‑Stokes方程描述速度、压力、黏性和外力怎样共同决定流体运动。问题的核心不是“能不能算出某一天的天气”，而是从平滑初始状态出发，三维流体速度是否可能在有限时间内变得无界。官方方案描述了一个不断向内盘旋、同时被拉长的涡旋：中心区域缩小、速度增大，但总能量仍保持有限；多个巨大项必须精确抵消，使外力继续光滑。
Lean则像一位极其严格但不懂物理直觉的检查员。人们把定义、引理和推导写成机器可验证对象，内核逐步检查每个结论是否由前提推出。它能排除许多“显然可得”的跳步，却不会自动证明你形式化的是正确版本的问题。
普通人和开发者会受到什么影响
对普通人，这件事不会明天就让飞机更省油或天气预报更准。数学定理到工程改进之间还有漫长链条。更现实的影响是科研组织方式：未来研究者可能把大量时间用于定义问题、设计验证、挑选值得追踪的分支，而不是亲手尝试每一条推导。
对开发者，一个直接类比是AI生成代码。单元测试通过只说明满足已写出的测试，不说明需求完整；Lean通过也只说明满足已形式化的命题。比如你让代理证明一个缓存协议“不会丢数据”，如果模型悄悄把断电场景排除，证明可以完全正确，系统仍可能在现实中失败。
我的判断及依据
我的判断是，这一事件即使后来需要修订，也已经展示了“计算规模换研究搜索宽度”的新范式。依据不是尚待确认的最终数学地位，而是公开链路中已经出现并行探索、跨组汇总、书面证明与形式化验证四个环节。下一步决定可信度的，不是更多宣传材料，而是第三方能否检查代码、重建定义并指出薄弱处。
适用边界与风险
不要把形式化验证写成“绝对正确”，也不要把供应商内部模型的表现外推到公开产品。论文可能存在形式化目标偏差、隐含假设或库层错误；大规模代理的Token消耗也意味着这种路线目前成本极高。数学共同体的接受通常需要时间，任何“已经获得千禧奖”的表述都不准确。
给研究团队的验证清单
- 保存原题、形式化定义与二者的逐项对应说明。
- 让未参与生成的专家独立阅读，而不是只看模型总结。
- 在不同Lean环境中重建依赖并锁定版本与哈希。
- 主动寻找反例、边界条件和被排除的物理情形。
- 分开记录“机器检查通过”“同行认可”和“权威机构确认”。
当AI能生成形式化证明时，你认为学术界最该新增哪一道独立验证程序？
关注「蜗牛聊AI」，一起看懂技术变化背后的真正机会。
本文首发于 java4u.cn，转载请注明出处。
