时间线
- 8.5
OpenAI一口气放出722篇AI数学手稿，数学界开始验收
OpenAI 公开了一批由未发布内部前沿模型产出的数学手稿，共 722 篇，来自约 4000 个开放研究问题的评测；不少手稿围绕同一核心结果展开，合并后对应 372 组相互关联的结果。其中几项直接触及长期未解决的重要问题：Unique Games 猜想的证明、被称为「准黎曼猜想」的结论（黎曼 ζ 函数在实部大于 7/8 的区域没有零点）、CM 阿贝尔簇上的有理 Hodge 猜想，以及 1940 年代以来悬而未决的自由群因子问题。 这次发布延续了一系列由 AI 产出的成果，既让数学界部分人感到振奋，也引发不安，同时把若干长期未解的问题摆到数学家面前等待审验。OpenAI 表示不同结果的验证程度并不一致，参与发布咨询的独立数学顾问组 AGMAI 也明确表示没有为这些结果背书，因此这些结论尚未成为定论。 这批手稿来自约 4000 个开放研究问题的评测，由未发布的内部前沿模型产出。Unique Games、准黎曼和自由群因子等结果已附上 Lean 形式化证明，可由计算机检查证明过程；而 OpenAI 表示没有形式化证明的部分仍可能存在错误。
- 9.0
分享人工智能在数学领域的进展
OpenAI 在 GitHub 上公开了名为 openai/math 的代码仓库，其中包含由 OpenAI 内部模型生成的数学手稿及配套证明材料，并附有 Lean 形式化证明。内容涉及多个长期未解的开放问题，例如 Barnette 猜想和 Unique Games 猜想。 Hacker News 的评论者认为此次发布意义重大：有人指出 Unique Games 猜想是“计算复杂性理论中的奠基性猜想”，也是许多不可近似性结果所依赖的假设，若证明成立“是件大事”。另一位评论者表示，自己几个月前曾花大量时间用当时最先进的模型尝试攻克 Barnette 猜想，但未能成功。 一位评论者引用 proofatlas.ai 称，该清单声称完整解决了数学领域前 500 个开放问题中的 90 个，其中排名最高的包括有理数域上的希尔伯特第十问题、Unique Games、Anderson 模型扩展态、时空 Penrose 不等式以及 Landau–Siegel 零点不存在性。另一位评论者特别提到三台机器单位作业调度的多项式时间算法，该问题自 1979 年 Garey 与 Johnson 的书出版以来一直未解。上述细节均来自社区讨论，并非对证明的独立验证。