OpenAI 的“十项进展”：数学与理论计算机科学

OpenAI 宣布 GPT-6 Astra 产出了十项结果，从球堆积上界到 Ramsey 数，并附有 Lean 证明；这些结果都未经同行评审，其中两项还受到数学家关于学术署名的质疑。

问题
十个开放问题，包括球堆积上界、非 sofic 群、Connes 刚性猜想和多色 Ramsey 数等
贡献方
GPT-6 Astra（OpenAI） · 论文由人与模型共同撰写；Lean 证明由模型编写
验证
已公开 Lean 证明部分独立审查（arXiv:2608.14673）
时间线
2026-08-01 宣布 → 2026-08-05 Lean 仓库 → 2026-09-09 审查第 3 版
来源
OpenAI 公告Lean 证明独立审查（arXiv:2608.14673）
待核实有 Lean 证明 · 未经同行评审 · 署名有争议

问题

OpenAI 于 2026 年 8 月 1 日宣布，其 GPT-6 Astra 模型在开放问题上产出了十项结果：

  1. 球堆积上界，直到 Cohn–Elkies 阈值。
  2. 二元码和球面码的界获得指数级改进。
  3. 非 sofic 群的存在性。
  4. 否定了 Connes 刚性猜想。
  5. 算术电路和公式中积和式（permanent）的下界。
  6. 双人量子博弈的指数级并行重复。
  7. 最近向量问题的多项式因子近似困难性。
  8. 所有维度下的 Ehrhart 体积猜想。
  9. 多色三角形 Ramsey 数的超指数下界（Erdős 问题 #183）。
  10. 极值图论中的紧性与退化猜想（Erdős 问题 #146 和 #180）。

AI 做了什么

据 OpenAI 介绍，按其 API 价格计算，算力成本约为 2,000 美元。论文由人与模型共同撰写，随后由模型编写 Lean 证明。

如何验证

Lean 证明已经公开。一项独立审查（Sienicki 与 Sienicki，arXiv:2608.14673）没有在主要结果中发现经确认的实质性错误，但审查深度不一：有一章被专家要求大幅修改；关于 Connes 猜想和最近向量问题的结果已得到后续工作的佐证。十项结果都未经同行评审。

局限

《科学美国人》（2026 年 8 月 6 日）报道了数学家对署名的质疑：Stephen Miller 表示，球堆积的证明依赖于他与合作者 2016 年的论证，却没有给予应有的署名；Francesco Fournier-Facio 表示，非 sofic 群证明的关键一步结合了 2016 年和 2019 年两篇论文的想法。OpenAI 修改了最初"至少十年没有进展"的说法。Lean 只能证明形式化后的陈述。在这些结果被逐一评审之前，我们将这一组记为"待核实"。

∎