AI 平均 3 小时完成一个数学证明，科研进入大通胀时代？

文 | 数智奔流，作者 | 田渝，编辑 | 沈校

美东时间 10 月 6 日傍晚 6 点，OpenAI 发布了由一款尚未公开的内部模型撰写的 722 篇数学研究手稿，这些手稿被归纳为 17 个领域的 372 个成果类别，其中 162 篇还附有主结果的 Lean 形式化证明。

官方表示，每项成功结果消耗的算力相当于 ChatGPT Pro 思考 3 小时。

声明的成果清单包括四维 Kakeya 猜想、广义黎曼猜想相关问题、唯一游戏猜想、自由群因子同构问题、有理数域上的希尔伯特第十问题、CM 阿贝尔簇的霍奇猜想、马勒猜想……

然而，OpenAI 在数学界以大胆宣称和缺乏透明度而闻名，这次的发布引发了相当大的质疑。

OpenAI 发言人告诉《科学美国人》，公司还没有公开发布的全新模型，几乎所有的结果都是在向单个代理发出单一指令后生成的。如果属实，意味着前所未有的数学能力可能很快为普通人所用。

质疑随之而来。质疑的导火索，来自 9 月 8 日，OpenAI 声称解决纳维—斯托克斯千禧年难题。

纳维—斯托克斯方程，研究的是水、空气等流体的运动，广泛应用于工程与物理。

难题的核心是：如果三维流体一开始很平稳，按照纳维—斯托克斯方程运动，它会一直保持正常、平滑，还是可能在有限时间内突然出现速度或涡旋无限大的 " 奇点 "？

OpenAI 表示，" 我们的系统给出了解析证明和 Lean 形式化证明，表明初始静止且光滑的流体可在有限时间内产生奇点。流体受到光滑外力作用，而从静止到形成奇点的整个动力学过程中，其能量始终有限。

这一结果证明了千禧年大奖难题官方表述中的命题 "C"（以及 "D"）成立，从而解决了纳维 - 斯托克斯千禧年大奖难题。"

克雷数学研究所在 2000 年设立了这一难题，是全球七大悬赏难题之一，奖金 100 万美元。OpenAI 并不打算申领奖金。

智能体系统是 9 月 1 日启动的。9 月 5 日，首批智能体启动约 88 小时后，解答出炉。后来的 Lean 形式化验证由 GPT-6 Astra 完成，又花了约 17 小时。整个过程中，智能体共发出约 490 万条消息，消耗约 3000 亿输出 token。

就在 OpenAI 官宣消息的 12 小时前，纽约大学数学家特里斯坦 · 巴克马斯特和他在 Anthropic 任职的合作者莱文特 · 阿尔珀格先公开了相近成果，优先权争议随之而来。

两人先后用 Claude、Codex 等 AI 模型做研究，8 月 15 日做出关键结果，8 月 22 日完成 Lean 验证。巴克马斯特表示，OpenAI 是在听到传闻迅速投入大量 AI 代理并发布成果。

巴克马斯特认为 OpenAI 在成果发布、署名和优先权上处理不当，并称对方曾要求排除阿尔珀格；OpenAI 否认使用他们的私人数据，称研究是独立完成的。这场优先权争议目前尚无定论。

数学家表示，领先的人工智能公司 " 给人一种黑帮行为的印象 "。

9 月 21 日，该公司宣布将组建一个由数学家组成的独立顾问小组，就如何负责地发布人工智能生成的计算结果提出建议。

小组建议 OpenAI 应该公布这个结果背后的模型、具体的提示信息和计算时间。小组尤其批评了使用 " 专有内部模型 " 的人工智能公司，因为这些模型并未向数学家广泛开放。

可是，OpenAI 选择仅公布问题的平均计算时间以及一些额外的统计数据，而没有提供任何提示信息。

更大的问题在于，Lean 验证并不等于这些成果已经被数学界确认。

米兰比可卡大学副教授瓦莱里奥 · 卡普拉罗发贴称，有最新论文研究发现，OpenAI 纳维—斯托克斯方案的论文和 Lean 代码至少有两处不一致：

论文中的一个估计只需要四个额外的输入导数，Lean 版本却需要五个，形式化结果因此更弱；论文中的压力—通量估计，也采用了不同的界限和证明方法。

卡普拉罗表示，目前不清楚这些差异是否会使整个证明无效，但它们引出一个重要问题：OpenAI 不断向我们宣称革命性突破，但没人知道这些证明是否正确，或者它们是否证明了它们声称要证明的内容。

就像卡普拉罗说的，Lean 验证的能力边界正在于此。Lean 只能检查这段数学推导在形式上有没有逻辑错误，判断不了它证明的内容是不是原来那个难题，也不能判断这个结果有没有真正的新意。

这也是为什么数学家要求公开完整的模型、提示词和计算过程，外界需要知道代码能否运行，需要逐项比较论文、形式化陈述和最终证明，确认三者是否指向同一个数学问题。

OpenAI 公布的 " 平均每项结果消耗约 3 小时 ChatGPT Pro 算力 "，也不能等于人工智能用 3 小时时间就解决了一道数学难题。

3 小时只是成功保留结果的平均计算量，模型还经历了问题筛选、方向探索、反复尝试和结果整理。OpenAI 的发言人也向《科学美国人》承认，部分成果可能经过多次尝试。

麻省理工学院的数学家安德鲁 · 萨瑟兰因此表示：" 除非他们公布模型，并且人们能够复现他们的结果，否则我认为任何关于用单个智能体一次性解决问题的说法都应该被视为未经证实，"" 我们应该要求他们提供证据。"

数学从来不只是获得答案。陶哲轩曾写道，在大量使用 AI 的时代，" 记住当一个孩子是什么感觉 " 十分重要；在他看来，纯数学尤其依靠好奇心、探索和孩童般的惊奇。

AI 正在改变数学活动的重心：当生成答案越来越容易，理解结果、提出好问题、判断其意义，并把新成果纳入人类知识体系，就变得更加重要。

这个重心正在经受 " 证明过剩 " 的考验。OpenAI 在发布 722 篇数学手稿后，因发现一个符号错误撤回其中 3 篇，并修改了另外 14 篇；目前仓库列出 719 篇。

数学家们没有足够的时间逐项阅读这 700 多篇手稿，更何况其中很多都是上百页的证明文本。这反映出数学界对 AI 竞赛最深的担忧：AI 正在制造 " 证明过剩 "，偏偏人类没有足够的时间和能力去理解这些证明。

验证，从来都是整个数学研究过程中最耗人心神的环节之一。

开普勒猜想证明本身得到认可后，仍用了十多年进行形式化验证；四色定理的答案早已得到广泛接受，但如何让数学共同体信任、检查并重建计算过程，持续了几十年；有限单群分类定理的单个结论的背后是一整个需要几代人维护、修补和整理的知识网络……

OpenAI 一次性放出 700 多篇手稿，等于把这套缓慢的消化流程压缩到了一夜之间。

有网友把这种发布方式称为 " 把未经证实的工作倾倒给数学家 "，也有乐观的声音认为，即使只有一半结果最终成立，这批成果仍可能改变数学研究。

" 如果我们想知道这些数学问题的答案，我看不出有什么理由要求公司对我们保密，" 多伦多大学数学家丹尼尔 · 利特说。" 在我看来，这对数学发展是一件好事。"

陶哲轩及一众菲尔兹奖得主签署的《人工智能与数学的严重错位》中提到，解决问题只是数学研究的一个工具，数学更重要的目标是概念理解、理论发展、人才培养和知识传承。

OpenAI 不会放慢脚步，它们希望为数学家们提供尽可能强大的工具。可是对于那些将数学真理视作目的的数学追求者来说，AI 竞赛的后果难以预测。