OpenAI 未发布模型 Astra 攻克 10 个数学未解难题：附 Lean 可验证证明，数学家社区震动

2026 年 8 月 1 日，OpenAI 通过官方博客宣布，其未发布的下一代模型系列 Astra 的内部版本在数学与理论计算机科学领域取得了 10 项新成果，全部附带 Lean 4 机器可验证证明并开源至 GitHub。OpenAI 称生成这些证明所消耗的 token 成本按 Sol API 价格计算总计约 2,000 美元。

核心成果

这 10 项结果涵盖高维几何、编码理论、群论、算子代数、量子复杂性、格密码学和极值组合学。其中最引人注目的包括：

非索菲群的存在性：构造了首个明确的非索菲群（non-sofic group），解决了自 1999 年 Gromov 提出索菲性概念以来悬置 27 年的群论核心问题。
Connes 刚性猜想的反证：推翻了关于特定群由其 von Neumann 代数唯一确定的长期猜想。
高维球体堆积上界：自 1978 年以来首次改进 Cohn–Elkies 阈值的一般上界。
三个 Erdős 问题：包括问题 183（多色三角形 Ramsey 数的超指数下界）、问题 146 和问题 180。
最近向量问题（CVP）的多项式因子不可近似性：这一结果触及基于格的抗量子密码学的基础。

OpenAI 同时发布了一份 249 页的完整论文、每个结果的推理过程叙述（reasoning walkthrough），以及 GitHub 仓库 openai/ten-proofs 中的 Lean 4 形式化验证证书。

社区反应

曼彻斯特大学数学家、erdosproblems.com 维护者 Thomas Bloom 在 X 上称此为"重大新闻"（Big news），并认为其重要性超过今年 5 月 OpenAI 模型推翻 Erdős 单位距离猜想的成果。"也许没有证明单位距离猜想那么重大，但就构造而言，这是大事，"Bloom 写道。他同时反驳了 AI 正在取代数学家的说法，指出"用一个数学家提出的猜想、用一个多世纪以来数学家发展出的理论、由数学家构建的 AI，并经过所有数学家所写内容的训练——将其称为'取代数学家'是不对的"。

菲尔兹奖得主 Timothy Gowers 在 X 上与 Bloom 的互动中，评价非索菲群的结果在"较弱的意义上是核心问题——该领域大多数人知道这个问题，并会对其被解决感兴趣，但它并不会真正改变该领域"。

OpenAI 推理研究负责人 Noam Brown 在 X 上确认，团队也尝试了其他重大问题但未成功："遗憾的是，还没有千禧年大奖问题（yet）。"他补充道："我们并没有在每个问题上花太多钱。把测试时计算进一步推高是可能的。"Brown 称 Astra 是"科学推理的重大一步"。

关于 Gowers 背书与验证的说明

此前在 2026 年 5 月，OpenAI 曾宣布同一模型系列推翻了 Erdős 单位距离猜想。彼时，菲尔兹奖得主 Timothy Gowers 公开表示愿毫不犹豫地推荐该证明发表于《数学年刊》（Annals of Mathematics）。数学家 Noga Alon、Melanie Wood 和 Thomas Bloom 参与了该项成果的独立验证。但需注意：Gowers 的 Annals of Mathematics 推荐和 Noga Alon 的验证均针对 5 月的单位距离猜想，而非本次 8 月 1 日公布的 10 项成果。截至目前，Gowers 尚未就本次 Astra 10 项成果发表类似的正式背书。

未解决的透明度问题

Hacker News 上的讨论反映了数学社区和 AI 观察者的几点质疑：

$2,000 成本口径：OpenAI 披露的是成功推理的 token 成本，但未说明总共尝试了多少问题、失败了多少次、以及搭建实验框架（harness）的额外成本。Noam Brown 承认"确实尝试了其他未成功的问题"，但未给出具体比例。
问题筛选：这些问题经过了适配 AI 能力的筛选，并非随机抽取。10 个结果来自一个更大的候选问题池，但 OpenAI 未披露完整的问题列表和筛选标准。
人类参与程度：OpenAI 表示"数学模型生成了数学论证，人类与同一模型合作将其整理为论文"。人类介入的具体深度——包括提示工程、结果筛选和编辑——尚不完全透明。

署名与归因立场

OpenAI 在博客中明确表态：声称"人类作者"完成了一个完全由 AI 生成的证明，将同时歪曲系统的贡献和真正人类智力工作的性质。这一声明直接回应了 2026 年 6 月数学界发布的《莱顿宣言》（Leiden Declaration），该宣言警告 AI 公司绕过同行评议、通过新闻稿发布成果的行为。值得注意的是，Gowers 参加了莱顿研讨会但最终未签署宣言，并在博客中解释了其立场。

政策与发布背景

据 The Decoder 报道，Astra 预计将成为首个通过美国政府 TRAINS 框架审批的 AI 模型。Altman 此前已在华盛顿向国会议员闭门展示了该系统。8 月 1 日 Musk 在 X 上发帖称"Grok 4.5 在考虑速度和成本时是帕累托最优"，虽然未直接提及 Astra，但发布时机被部分观察者视为对 OpenAI 数学成果的间接回应。

保留判断

Astra 模型尚未公开发布，外部无法独立复现其推理过程。所有证明虽然通过 Lean 4 机器验证，但证明本身的数学意义和优雅性仍待学术同行评议。
问题的选取和实验框架的完整披露对于准确评估 AI 的数学推理能力至关重要，目前这些信息仍不完整。
本次成果与此前 5 月的单位距离猜想反证共同构成了 AI 数学推理能力的关键证据链，但两项成果均来自同一未发布模型系列，独立验证存在天然局限。