OpenAI 周二在 GitHub 发布了 722 篇数学手稿，称这些内容全部由一款尚未发布的内部模型生成。OpenAI 发言人表示，几乎所有结果都来自交给单个 AI 代理的一次提示，不过其中部分结果可能经历了多次尝试。
这一说法在数学界引发了不小反响。支持者将其视为潜在突破，质疑者则把焦点放在模型未公开、结果难以复现，以及验证材料仍不完整。
722 篇并不等于 722 道已解难题
这批论文被归入 372 个相互关联的「家族」。一个家族可以包含主定理、配套论证、推论或替代证明，因此 722 这一数字对应的是手稿数量，而不是已解决问题的数量。
OpenAI 表示，公司向该模型提出了大约 4,000 道问题，最终保留并发布了其认为足够重要的输出结果。
按 OpenAI 的说法，平均每项结果消耗的推理算力，大致相当于 ChatGPT Pro 约 3 小时的思考计算。相比之下，上个月涉及 Navier-Stokes 的那项声明采用的是完全不同的方式：10,000 个协同代理运行了 88 小时。
形式化验证覆盖率约 22%
OpenAI 为其中 10 项结果公开了删节版推理摘要。不过，根据仓库中的形式化目录，722 篇手稿里只有 162 篇附带了经过计算机检查的主结果，占整个集合约 22%。这些结果被翻译为 Lean 代码，由该软件逐步机械检查逻辑链条。
OpenAI 也明确表示，并非所有手稿都完成了 Lean 形式化，而且「一些未形式化的结果可能存在问题」。换句话说，这次公开的内容中，仍有相当一部分可能并不正确。
即便通过 Lean 检查，也只能说明证明在 Lean 中按写定的命题能够成立，并不能证明该命题与原始问题完全一致，也不能证明结果具有新颖性或重要性。这部分判断，仍需要数学家来完成。
数学家要求公开更多可核查材料
麻省理工学院数学家 Andrew Sutherland 对《Scientific American》表示：「在他们公开模型、让其他人能够复现结果之前，我认为，任何关于单个代理通过一次尝试就解出问题的说法，都应被视为未经验证。」他还说：「我们应该要求他们拿出凭据。」
研究人员的质疑很快出现在公开讨论中。Dmitry Rybin 在 X 上表示，他尝试阅读 OpenAI 关于「平面色数大于等于 6」的证明，但认为这份证明呈现出一种「完全难以置信的外星数学」风格。他写道，模型似乎得出了「任意 K-着色当且仅当『弱可测』K-着色」这一结论，而这一点看起来来得毫无来由。
Keith Adler 则指出，openai/math 仓库关闭了 Issues，且从未接受过任何 pull request。他表示这令人失望，因为如果 OpenAI 一次发布 722 篇手稿，并希望外界补充 Lean 形式化，就应该提供一个提交渠道。他还提到，自己正在用 Lean 4 形式化 OpenAI 对 Saxl 猜想的证明。
高等研究院：数学的人类理解仍然至关重要
位于美国新泽西州普林斯顿的高等研究院在一份声明中表示：「现在已经出现这样一种情况：AI 可以在提示它的人类无法理解、无法验证、也无法为之负责的情形下，输出数学论证。」该机构还表示：「我们认为，人类对数学的理解仍然具有至关重要的意义。在这个新时代，我们如何推动一种新范式，把人类对数学的理解纳入负责任的学术产出之中？」
这份表态把争议进一步拉回到学术责任问题：如果结果来自人类难以解释的推理链条，那么公开、审查和署名应如何处理，仍没有现成答案。
也有数学家称这是「数学的大日子」
并非所有反馈都偏向保留态度。Abhishek Saha 教授写道：「这是数学的一个非常重要的日子。」不过他也补充说，这批问题中的大多数更适合归入「现有研究计划中的特殊进展」，而不是「令人意外的突破」。
按这一判断，这组问题大多具有研究价值，但并非千禧年难题那种几乎不可能、足以改写领域格局的级别。在 722 篇手稿中，只有一个问题被放在这一层级：Quasi-Riemann Hypothesis。
Saha 在另一则帖文中还表示，他对 OpenAI 当天发布的 372 项结果、共 722 篇手稿做了进一步思考，并尝试按突破性强弱对数学家发表的定理进行粗略分类。
公开内容仍低于外部建议标准
这次发布也没有达到高等研究院一个顾问小组在 9 月 29 日提出的建议标准。该小组当时建议，对每一项结果都公开模型名称、提示词、摘要化思维链、耗时和计算成本。
OpenAI 目前公开了平均算力数据和 10 份推理摘要，但没有公开提示词，并表示公司仍在推进以负责任的方式发布该模型。
多伦多大学数学家 Daniel Litt 则持相反看法。他认为，没有理由要求公司把这些数学问题的答案继续保密。
与 Anthropic 的做法形成对照
上个月，Anthropic 在处理经 Lean 检查的费马大定理证明时采取了不同路径：公司把全部 1,300 万行内容公开发布在 GitHub 上。不过，那份证明形式化的是 Andrew Wiles 在 1995 年发表的一个定理，而不是宣称获得新的数学结果。
OpenAI 表示，随着后续取得更多成果，公司会继续补充 Lean 形式化。现阶段，722 篇手稿中已有 162 篇附带这类形式化材料。