OpenAI 宣布一个尚未发布、能力显著超过 GPT-6 Astra 的下一代模型

小甲鱼的二师兄

通过约 1 万个 AI agents 协作，仅用 88 小时构造出一份 Navier–Stokes 千禧难题的反例证明：

某种原本完全光滑、甚至从静止开始的三维流体，在受到光滑外力作用后，可以在有限时间内产生 “奇点”，即速度趋向无穷大。OpenAI 同时公开了数学论文和 Lean 形式化证明。

不过，目前它仍然是一个刚刚公布、等待数学界审查的 “候选解决方案”，还不能说已经获得 Clay 数学研究所正式认证。

FishC

结论：先别把它当成“千禧难题已解决”。

这条描述最多只能算“候选方案/待核实消息”。模型未发布、能力无法独立验证；AI agents 数量多、耗时短，也不是数学证明可信的理由。

关键要看这几点：

• OpenAI 是否有正式公告、论文和可复现材料。
• Lean 形式化证明是否能公开编译通过，是否有 sorry、额外公理或定义偏差。
• 形式化证明的对象，是否严格对应原始 Navier–Stokes 千禧难题。
• 是否有独立数学家同行评审，而不是只靠官方自述。
• Clay 数学研究所是否正式认证。
  

为什么 Lean 证明很强，但仍不能直接封神？
Lean 只能保证“代码里的定理”被机器检查通过。它不能自动保证：形式化定义没问题、前提条件没被偷偷加强、原始问题被准确翻译。数学界仍需人工审查。

给鱼油的判断口诀：

• 原始论文在哪里？
• 证明能否独立复现？
• 权威机构认了吗？
  

三样都齐了，才可以说“基本可信”。现在只能说：如果是真的，这是世纪级成果；但在正式审查和 Clay 认证前，它只是候选解决方案。

以上回复来自 FishC AI 小助理，如未能正确解答您的问题，请继续追问。