OpenAI Astra：2000 美元 + Lean 证书解决 10 个数学难题，这比”AGI 又近一步”更值得讨论的是研究范式迁移
分类：paper · AI 推理 / AI for Math 时间：2026-08-01 OpenAI 官方发布 信源：OpenAI 官方 249 页 PDF（cdn.openai.com）、GitHub openai/ten-proofs 仓库（Lean 4 形式化）、aiweekly.co、Decoder
数字
– 10 个结果，涉及高维几何、编码理论、群论、算子代数、量子复杂性、格密码学、极值组合学。 – 总推理 token 成本，按 Sol API 价折算约 2000 美元。 – 每条结果附一份 Lean 4 形式化证书（机器可逐行核查）。 – 全部论证、Lean 证书、思维过程说明在 GitHub 公开：https://github.com/openai/ten-proofs
清单（10 项）
1. 高维球堆积：把堆积密度的指数推到 Cohn–Elkies 阈值一线，是 1978 年以来首次改进。 2. 二元码与球面码：对所有参数把码最大规模上界改进了指数级因子。 3. 非 sofic 群：构造显式反例，否定”每个可数群都允许有限置换逼近”。 4. Connes 刚性猜想：构造出无数两两不同构但共享同一 von Neumann 代数的群，猜想被否证。 5. 算术电路复杂性：给 permanent 的公式规模 n⁴/log n 下界。 6. 量子并行重复：把指数型并行重复定理推广到任意有限两人纠缠博弈。 7. 最近向量问题：从 3SAT 出发的直接归约给出多项式因子近似困难性。 8. Ehrhart 体积猜想：对重心是唯一内部格点的凸体，每个维度都证明精确上界。 9. 多色 Ramsey 数：超指数下界解决 Erdős 第 183 号问题。 10. 极值数猜想：与第 9 项相关的极值图论方向进展。
这件事比”AI 又攻克一个难题”重要在哪里
过去一年里，”AI 解开数学难题”这种标题出过不少次。一部分后来被发现问题早有文献、或者证明本身有漏洞、或者 AI 只是”复述”已知证明。
OpenAI 这次做对了两件事：
1. 形式化进 Lean 4
机器可核查的证明证书不再是”作者说了对就对了”。Lean 4 社区已经审过 8 万+ 行形式化证明，包括 Sphere Eversion、liquid tensor experiment、Busy Beaver 上界这些。Lean 4 不能告诉你这个证明解决了”你想解决的问题”，但能告诉你每一步推导是否逻辑成立。这把”AI 解题”过去最常被质疑的”中间步骤跳步”问题，从根本上消除了。
2. 把人类研究人员的角色说清楚
OpenAI 这次把话说得相当直白：论证由模型生成，人类研究者做的是”把论证整理成论文手稿”。Lean 证书也是模型自己从自己的论证里转换过来的。署名规则、知识产权规则都基于这个事实来。
2000 美元这个数字意味着什么
之前”AI 解开未解数学难题”的成本表述通常是”数百万美元 GPU 时 + 顶尖团队”。
Astra 跑完这 10 个问题，按 Sol API 价折算总 token 约 2000 美元。这不是训练成本，是推理时消耗的 token 折算值。即使加上研究人员的工资、Lean 转换的工程成本，单题”单点突破”的边际成本从”博士论文级”降到”云账单级”。
研究范式的迁移在这个数字上：
– 过去 1 个博士花 5 年攻 1 个开放问题。 – 现在 1 个研究员 + 1 个模型 + 1 个 Lean 验证器，几个星期可以同时铺开几十个候选问题。
Astra 是 OpenAI 内部模型，研究员 Sebastien Bubeck 在 X 上说”这只是示意，不是 Astra 已经做到的全部”。换句话说，这只是 OpenAI 愿意公开的那一小部分。
限制
– 全部 10 个结果数学界还没有足够时间审完。Lean 4 证书保证逻辑正确，不保证”形式化的命题就是数学家关心的那个命题”。一个常见的争议点是”你把命题翻译成形式化时，可能已经把它换成了一个更弱的版本”。 – 没有公开 Astra 模型权重、训练数据、训练成本。后续数学家要做同行评审，只能从”模型输出了什么”反推”模型是怎么输出的”，这是天然的信息不对称。 – “攻破”的字面意义在数学界有争议。Connes 刚性猜想被否证是真正的反例；但球堆积、二元码上界这种”渐进改进”在数学界更常被称为”重要进展”而不是”解决问题”。 – 这次发布 10 个问题是 OpenAI 主动筛选的，Astra 在哪些问题上”翻车”没有公开。
一个更长远的判断
腾讯混元 Hyra 7-31 解的是 50 年加法组合学猜想，走的是”AI 搜索 + 人类封顶 + Lean 形式化”三段式；小红书 dots 7-23 IMO 满分不依赖 Lean 直接读 LaTeX；OpenAI Astra 这次是”AI 出论证 + AI 转 Lean + 人类整理论文”。
三家的共同点：Lean 形式化从加分项变成了默认配套。这是 AI for Math 这条线在 2026 H2 最明显的范式转移——没有 Lean 证书的”AI 解题”现在基本没人信。
下一步值得看：数学界对 Astra 这 10 个结果的同行评审结果，以及 Astra 是否会在某个时间点对外开放 API。
原文链接： – https://openai.com/index/ten-advances-in-mathematics/ – https://cdn.openai.com/pdf/ten-proofs-oai.pdf – https://github.com/openai/ten-proofs – https://aiweekly.co/alerts/openai-releases-ten-astra-math-proofs-with-lean-certificates – https://the-decoder.com/2026/08/01/openai-ten-math-proofs