OpenAI 未发布模型 Astra 连破十道数学难题，全部附 Lean 可验证证明

2026 年 8 月 1 日，OpenAI 数学研究负责人 Sebastien Bubeck 在 X 上发了一条推文，开头只有四个单词和一个冒号——"yes, nonsofic groups exist"（Bubeck，8 月 1 日）。Bubeck 称这些结果是 Astra——OpenAI 下一代主要模型——的"beautiful results"。两天后，OpenAI 官方账号正式宣布：该模型的一个内部版本在数学与理论计算机科学的十个长期开放问题上产出了新结果，使用的 token 按 GPT-5.6 Sol API 费率计算约 2000 美元。

伴随公告，OpenAI 在 GitHub 上以 Apache 2.0 许可证发布了 249 页研究手稿和全部十项结果的 Lean 4 证明证书。据 Quartz 报道，该仓库的 "sorry" 计数为零——在 Lean 证明助手中，"sorry" 表示一个跳过的证明步骤，零意味着每一步都已被形式化验证。

十个结果分别做了什么

十项结果横跨几何、群论、编码理论、算子代数、量子复杂性、格密码学和极值组合学。根据 OpenAI 发布的 249 页 PDF 手稿，全部列出如下：

非 sofic 群的存在性：构造了首个显式的非 sofic 群，终结了自 Mikhail Gromov 1999 年提出 sofic 概念以来悬而未决的问题。证明使用了 property-(T) expander 和二元 Leavitt 代数。

Connes 刚性猜想的否证：构造了无穷多对具有相同群 von Neumann 代数但互不同构的 property-(T) 群，推翻了 Alain Connes 的刚性猜想，同时回答了 Sorin Popa 的一个相关有限性问题。

高维球堆积：精确确定了 Cohn–Elkies 线性规划的渐近衰减率，给出了自 1978 年以来高维球堆积上界的首次改进。新指数为 α* = 0.6044…，优于经典的 Kabatianskii–Levenshtein 指数 0.599…。

二元码与球面码：对所有参数以指数级因子改进了固定距离二元码和球面码的经典上界。

Ehrhart 体积猜想：在任意维数下证明了 (n+1)^n/n! 的精确上界，解决了 barycenter 是唯一内部格点的凸体的最大体积问题。

多色 Ramsey 数：证明了 R_k(3) = k^Θ(k) 的超指数下界，解决了 Erdős 问题 183。

算术电路复杂度：证明了计算 permanent 的除零电路需 Ω(n² log log n) 个门，公式需 Ω(n⁴/log n) 个叶节点。

量子并行重复：证明了所有有限双人纠缠博弈的指数并行重复定理，将经典复杂性理论的基础原理扩展到一般量子博弈。

最近向量问题（CVP）：给出了从 3SAT 到欧几里得 CVP 的 n^{1/400} 因子困难的直接归约，对后量子密码学有直接影响。

紧性与退化猜想：分别构造了二部图反例，否证了 Erdős–Simonovits 紧性猜想和 Erdős 退化猜想（Erdős 问题 146 和 180）。

非 sofic 群：等了 27 年的答案

十项结果中，非 sofic 群的显式构造最受关注。sofic 群是 Gromov 在 1999 年引入的概念，核心问题是：是否所有可数群都能用有限置换来逼近？据 DataCamp 报道，多数发表意见的数学家将这项结果视为十项中最突出的，其重要性在于它是"27 年来第一个此类构造"。

Astra 给出的是"否"——构造了一个明确无法被任何有限逼近序列捕获的群。Quartz 引述 erdosproblems.com 维护者 Thomas Bloom 在 X 上的评价，称这十项结果是"大新闻"（big news），并将其重要性排在此前 OpenAI 模型在单位距离问题上产出的反例之上。

Sebastien Bubeck 在后续推文中点名感谢了多位参与训练该模型的 OpenAI 研究人员。OpenAI 研究科学家 Noam Brown 则在 X 上称这些结果是科学推理的重大一步（"a major step for scientific reasoning"）。

不是人类写的，但人类整理了手稿

OpenAI 明确区分了数学论证的来源与论文写作的责任。根据公司声明，模型的论证由 Astra 生成，人类研究人员随后将论证整理为可发表的手稿，并用同一模型将证明形式化为 Lean 证书。公司表示对工作的正确性承担责任，同时主张：如果一篇证明完全由 AI 系统生成，声称人类作者身份会同时曲解系统的贡献和人类智力工作的本质。

关于 2000 美元这个数字，OpenAI 说明了它的计算口径：这是生成十项已发表解的 token 成本，不包含 Astra 在过程中尝试但失败的其他问题所消耗的 token。

数学界：兴奋、质疑、以及更大的问题

社交媒体上的反应迅速分化。一部分人关注速度本身——十个问题在同一批结果中落地。一位 X 用户评论："OpenAI just speedran decades of math research for $2,000"。另一条回复更直白："University math and CS professors reading this"。

但也有批评声音。认知科学家 Gary Marcus 在 Substack 上撰文，标题为"OpenAI's amazing — but vastly oversold — new model Astra"，指出 Astra 在数学上的成功不等同于通用智能，数学是可形式化验证的特殊领域，"成功在一个领域不保证成功在所有领域"。

DataCamp 的分析文章讨论了围绕这批结果的一个常见质疑：几项结果是反例而非新的一般理论。但该文同时指出，非 sofic 群的构造并非对已有近似构造的小幅修改，而是 27 年来无人拥有的首个构造；球堆积上界和 CVP 困难度结果也根本不是反例，而是对已有上界的直接改进。

更深层的争议来自国际数学界与 AI 公司之间的结构性矛盾。Quartz 报道称，国际数学联盟（IMU）6 月签署的莱顿宣言正式表达了数学界的担忧：AI 公司在未经许可的情况下利用已发表研究进行训练，绕过同行评审，并侵蚀了围绕证明和署名的学术标准。

Lean 的形式化验证提供了一个折中方案：任何人都可以运行编译器来检查证明的逻辑一致性，无需等待期刊审稿。但正如 DataCamp 所指出的，Lean 只能保证步骤间的逻辑自洽，无法独立确认问题被形式化的方式是否与数学家所意图的一致——这仍然需要人类审稿人来判断。

没有审稿，没有时间表

OpenAI 尚未公布 Astra 的发布时间，也未明确该模型最终会以 GPT-6 还是 GPT-5 系列的面目出现。根据 Quartz 的报道，Astra 需要先通过联邦 AI 安全审查才能面向用户。

据 Quartz 引述 SiliconAngle，十项结果目前均未经过正式同行评审。OpenAI 在公告中表示，希望数学界能够审视这些结果、将其置于学科脉络中，并在这些想法的基础上展开进一步研究。这是否会发生、以多快的速度发生，将在很大程度上决定这批结果在数学史上的位置。

参考链接

• OpenAI 官方推文，2026 年 8 月 3 日
• Sebastien Bubeck 推文，2026 年 8 月 1 日
• OpenAI 官方博客：Ten advances in mathematics and theoretical computer science
• OpenAI PDF 手稿：Ten Advances in Mathematics and Theoretical Computer Science
• GitHub 仓库：openai/ten-proofs（Lean 4 证明证书）
• Quartz：OpenAI Astra model solves 10 open math problems for $2,000
• The American Bazaar：OpenAI says AI system advances 10 major math problems
• DataCamp：OpenAI's New Model, Astra, Has Solved Ten Open Math Problems
• Gary Marcus Substack：OpenAI's amazing — but vastly oversold — new model Astra