AI提交千禧难题证明，真正的门槛转向公开验证
内容提要
OpenAI称其内部AI系统给出了Navier-Stokes方程的反例，并附有Lean形式化证明，但克雷研究所仍将该问题标为未解决。文章指出，AI进入前沿数学后，关键不再是生成候选证明，而是建立公开、可信、可复核的验证链；形式化通过不等于原问题获证，仍需同行独立检查。
延伸解读
形式化验证不等于数学确认
文章强调，Lean形式化证明只能检查逻辑步骤是否符合编码后的公理和定义，但无法保证形式化的问题与原问题完全一致。基础库、定义选择或书面论证中的语义遗漏，都可能使证明偏离原意。因此，即使机器验证通过，仍需人类专家独立确认形式化目标是否准确，不能直接等同于原问题获证。
大规模代理协作的新研究范式
OpenAI披露的系统使用约1万个并发智能体，发送约270万条消息，消耗约1300亿输出Token，候选解在约88小时后出现。这显示AI数学研究正从单模型推理转向大规模并行探索与跨组汇总。但文章提醒，这些数字是供应商披露，尚未独立复现，且Token消耗意味着该路线目前成本极高。
对开发者的直接类比：测试通过≠需求满足
文章将Lean验证类比为AI生成代码的单元测试：测试通过只说明满足已写出的测试，不说明需求完整。若模型在形式化时悄悄排除断电等场景，证明可以完全正确，系统仍可能在现实中失败。开发者应关注形式化目标是否覆盖真实约束，而非仅看验证结果。
可信度取决于第三方独立检查
克雷数学研究所仍将Navier-Stokes问题标为未解决，OpenAI也不申领奖金。文章指出，下一步决定可信度的不是宣传材料，而是第三方能否检查代码、重建定义并指出薄弱处。研究团队应保存原题与形式化定义的逐项对应，让未参与生成的专家独立阅读，并分开记录机器检查、同行认可与权威机构确认。
Q&A
OpenAI 是否已经解决了纳维-斯托克斯方程问题？
没有。OpenAI 于 9 月 8 日公布了一份解答，声称其内部 AI 系统构造了三维不可压缩流体的反例，并附有 Lean 形式化证明。但克雷数学研究所仍将该问题标为“未解决”，数学共同体也需要独立检查。因此不能认为问题已被解决。
OpenAI 的 AI 系统是如何发现这个纳维-斯托克斯反例的？
根据 OpenAI 披露，系统使用了约 1 万个并发智能体，发送约 270 万条消息，消耗约 1300 亿输出 Token。候选解在启动约 88 小时后出现，随后 Lean 形式化与验证又花了 17 小时。此前，较小规模（近 100 个代理）先在约 50 小时内得到了 Euler 方程正则性反例，成为后续集中资源的线索。
Lean 形式化证明通过是否意味着原数学问题被证明了？
不是。Lean 形式化证明只能检查逻辑步骤是否符合编码后的公理和定义，但无法确认形式化的问题是否与原问题完全一致、基础库和定义是否合适、书面论证是否遗漏关键语义。因此形式化通过不等于原问题获证，仍需人类独立检查。
这件事对普通人和开发者有什么实际影响？
对普通人，短期内不会直接改善飞机燃油效率或天气预报，因为数学定理到工程应用还有漫长链条。更现实的影响是科研组织方式的变化：研究者可能更多时间用于定义问题、设计验证和挑选分支，而非亲手推导。对开发者，类似 AI 生成代码：单元测试通过只说明满足已写出的测试，不说明需求完整；Lean 通过也只说明满足已形式化的命题。
研究团队应该如何验证 AI 生成的数学证明？
文章建议的验证清单包括：保存原题、形式化定义及逐项对应说明；让未参与生成的专家独立阅读；在不同 Lean 环境中重建依赖并锁定版本与哈希；主动寻找反例、边界条件和被排除的物理情形；分开记录“机器检查通过”“同行认可”和“权威机构确认”。
AI 进入前沿数学后，最稀缺的资源是什么？
文章的核心判断是：AI 进入前沿数学后，稀缺资源将从产生候选证明，转向建立可信、公开、可复核的验证链。也就是说，关键不再是生成候选证明，而是建立公开、可信、可复核的验证链。
