2026年9月8日，OpenAI在官方博客发布长文，宣称其内部旗舰模型GPT-6 Astra驱动的一万多个子代理在五天内完成了Navier-Stokes方程三维情况下的存在性与光滑性证明，称这一成果有望被评审为克雷数学研究所悬赏的七大千禧年大奖问题之一的正式解答。公告发布数小时后，纽约大学数学家Tristan Buckmaster在arXiv上传了一份标题相同的独立预印本，声称其团队在过去两年中独立完成了该问题的核心证明框架，并对OpenAI的成果原创性提出了公开质疑，一场数学与AI的归属权争议瞬间引爆学术界和技术社区。
成本与规模：五天烧掉1500万美元
OpenAI在技术报告中披露了令人瞠目的资源消耗数据：代理集群在五天运行周期内累计发送490万条消息，消耗约3000亿输出token。以GPT-6 Astra当前的API定价（每百万输出token 50美元）估算，仅推理成本就达到约1500万美元。OpenAI未公布该内部专用模型的具体架构，但确认其为GPT-6 Astra的一个特化版本，具备更强的形式化数学推理能力。社区评论者将这笔支出与全职数学家的年薪进行了对比：1500万美元相当于60到120名数学研究员一年的薪酬总和，这一类比引发了关于AI辅助数学研究成本效益的广泛讨论。
归属之争：独立成果还是训练数据泄露
争议的焦点在于OpenAI的代理是否在训练过程中接触过Buckmaster团队的工作草稿。Buckmaster在其正式声明中指出，他在过去一年中曾使用OpenAI的产品进行部分计算验证，其对话数据可能在不知情的情况下流入了模型的训练语料库。OpenAI的回应措辞谨慎但措辞模糊：官方声明中承认了"虽然可能性不大，但我们不能排除用户脱敏数据帮助改进模型的可能性"。这一表态反而加剧了社区的质疑，多位知名研究者在社交平台指出，如果证明过程确实借鉴了Buckmaster的工作，那么OpenAI的"攻克"宣称就存在严重的学术伦理问题。
形式化验证：机器可检查的证明
撇开归属争议，这次事件在技术层面确实展示了AI代理在形式化数学上的推进能力。OpenAI披露的工作流程显示，代理集群并非直接输出自然语言证明，而是生成可被证明助手机器检查的形式化代码，这一点与今年早前Anthropic用Lean完成费马大定理形式化的路径类似。形式化证明的优势在于正确性可以被自动验证，不依赖人类评审者逐行审读，这在数学界长期是一个耗时数年的瓶颈环节。多位形式化数学研究者指出，即便OpenAI的证明确实借鉴了已有工作，能够在五天内把一个千禧年级别问题的证明骨架转化为机器可检查的形式化代码，本身也是工程能力上的显著突破。
另一个被广泛讨论的技术细节是代理集群的协作机制。490万条消息意味着代理之间存在密集的中间结果交换和路径剪枝，这种大规模并行搜索在人类研究团队中根本无法复现——没有任何数学家团队能在五天内完成这个量级的沟通和验证吞吐。有评论者用"数据中心里的天才之国"来形容这一景象，也有人指出这恰恰暴露了当前范式的局限：靠算力穷举而非洞察力突破，本质上是用一千五百万美元换取了两名数学家两年的思考成果。
目前，克雷数学研究所尚未对这一成果作出任何官方回应，评审流程预计将持续至少一到两年。无论最终结果如何，这次事件已经为AI参与前沿数学研究的边界划下了一个具有里程碑意义的案例：当AI代理的计算能力强大到可以在数天内穷举形式化证明路径时，成果的原创性认定标准需要被重新定义。