OpenAI Astra 数学新结果：十项长期问题与 Lean 验证

AI数学Lean

2026 年 8 月 1 日，OpenAI 公布了一份名为《Ten Advances in Mathematics and Theoretical Computer Science》的论文，介绍内部版本 Astra 在数学和理论计算机科学中的十项新结果。OpenAI 的表述很克制：这些问题至少十年没有出现主要进展，多数问题的开放时间更久。

这份材料的看点不止是“十项”这个数字。十项结果的性质并不相同，有新的上界和下界，有对象构造，有猜想反例，也有复杂度与密码学问题上的硬度证明。它们共同展示了一条正在成形的研究流程：模型提出长论证，人类把论证整理成可读论文，再用 Lean 把形式化后的证明交给机器检查。

OpenAI论文摘要页，列出十项数学与理论计算机科学结果

十项结果覆盖了什么

官方论文的摘要把结果列成十项。下面按问题类型整理，并补上论文中的定量结论。

方向问题OpenAI 论文给出的结果
高维几何高维球体堆积精确确定 Cohn–Elkies 线性规划的渐近指数，改进高维一般球体堆积上界。论文称这是一般球体堆积指数自 1978 年以来的首次改进。
编码理论二元码与球面码对固定最小距离或最大内积的码，改进经典上界，并在所有参数上获得指数级改进。
群论非索菲克群构造一个明确的非索菲克群，回答“每个可数群是否都能用有限置换逼近”这一核心问题。
算子代数Connes 刚性猜想构造出两两不同构、却拥有同构群 von Neumann 代数的 property-(T) 群，反驳 Connes 猜想。
代数复杂度permanent 的电路与公式下界无除法电路需要 Ω(n² log log n) 个算术门，公式需要 Ω(n⁴/log n) 个变量叶子。
量子复杂度量子并行重复对所有有限的双人纠缠博弈证明指数级并行重复定理，扩展经典并行重复原则。
格密码最近向量问题从 3SAT 出发，得到欧氏最近向量问题在固定多项式因子内的近似困难性，论文给出 n 的 1/400 次方因子。
凸几何Ehrhart 体积猜想在任意维度证明尖锐上界 (n+1)^n/n!，适用对象是重心同时为唯一内部格点的凸体。
极值组合多色 Ramsey 数对 k 色三角形 Ramsey 数给出超指数下界，并得到 R_k(3)=k 的 Θ(k) 次方，解决 Erdős 问题 183。
极值图论紧性与退化性猜想给出两个二部图构造，分别反驳 Erdős–Simonovits 紧性猜想和 Erdős 的退化性猜想，对应 Erdős 问题 146 与 180。

其中有几项尤其容易被标题压缩掉。

高维球体堆积并非再次证明八维 E8 格或二十四维 Leech 格的最优性。论文处理的是高维一般情形，研究 Cohn–Elkies 线性规划在维数趋于无穷时能给出多强的上界。论文给出的极限是 (e/(2π))^(1/2)，并把一般球体堆积的指数上界推进到 1978 年以来没有出现过的区域。二元码和球面码的结果也沿着同一条线索推进：把高维编码问题中的经典指数上界再压低一截。

Connes 刚性猜想的结果更适合用“结构信息不足以唯一恢复群”来理解。猜想讨论的是：带有 ICC 和 property-(T) 条件的群，其群 von Neumann 代数是否能决定原群。论文构造了一个可数无穷族，两两不同构，但群 von Neumann 代数同构。这个构造直接击中了猜想中的唯一恢复关系。

算术电路复杂度部分讨论的是 permanent。它与 determinant 在表达能力和计算复杂度上的差异长期受到研究者关注。OpenAI 论文分别处理可复用中间结果的无除法电路，以及树形结构的公式，给出两组不同的下界。两个量级不能混用：电路允许复用，公式把每次变量使用都展开到叶子，因此证明对象和计数方式不同。

量子并行重复结果的语境是双人纠缠博弈。裁判独立重复同一个游戏多次，只有每一局都获胜才算整体成功。经典玩家的获胜概率会指数下降，纠缠会引入相关性与相位问题，使推广并不自动成立。论文称其证明覆盖所有有限双人纠缠博弈，而不局限于此前已经处理的特殊类别。

最近向量问题与后量子密码学有关。论文给出从 3SAT 到 GapCVP 的确定性多项式时间归约，目标是证明在欧氏格上进行最近向量近似存在固定多项式因子的困难性。这个结果的表达方式是复杂度理论语言，不能直接翻译成“某种密码已经被破解”；它讨论的是问题的近似计算难度。

Ramsey 数部分给出了一个很适合公众理解的量级变化。R_k(3) 表示使用 k 种颜色给完全图的边染色时，强制出现单色三角形所需的最小顶点数。论文证明其量级为 k 的 Θ(k) 次方，这意味着颜色数量增加时，避免单色三角形所需的图规模增长得非常快。

Lean 证明解决了哪一层问题

OpenAI 在网页中明确说明：Astra 生成数学论证，人类将论证整理成论文，随后模型把每项论证形式化为 Lean certificate。OpenAI 同时公开了 openai/ten-proofs 仓库，仓库中包含选定证明的 Lean 文件，以及一个逐项检查独立 Lean 解的 comparator 配置。

Lean 的作用是把命题、定义、引理和推导写进一个形式系统，再由证明助手检查最终证明对象。对于很长的数学论证，这一步可以捕获符号、量词、类型和推导链上的形式错误，也让第三方拥有可重复的机器检查入口。

保证边界也需要写清楚。Lean 检查的是已经形式化的命题和证明对象，数学界仍需审阅问题的表述是否准确、证明是否真正对应论文主张、使用的定义和假设是否合适，以及结果在相关领域中的创新性和历史归属。形式化验证提供了强证据，同行审阅负责建立学术语境，两者承担的任务不同。

这也是本次发布比普通“模型解出难题”宣传更有信息量的地方。OpenAI 没有把人类的整理、形式化和责任承担隐去，也没有把模型生成的数学论证改写成纯粹的人类成果。公司在原文中明确表示，归属应如实反映结果的产生方式，并由 OpenAI 对论文和形式化工作负责。

两千美元代表什么

OpenAI 给出的数字是：寻找这些问题解法所需的 token，按 Sol API 价格计算约为 2000 美元。这个数字应理解为 API 价格口径下的 token 成本估算，不能直接当作项目总成本，也不能当作每项证明的平均价格。

它仍然提供了一个有用尺度。十项问题横跨高维几何、群论、算子代数、复杂度理论、量子理论、格密码和极值组合，模型需要在长论证中保留上下文、尝试失败路径、切换数学工具，再把可用路线整理出来。OpenAI 公开的 reasoning walkthroughs 也把若干探索过程单独放出，读者可以把最终论文与模型的探索轨迹对照阅读。

这次发布的真正变量

对数学研究而言，模型给出一个结果只是起点。后续需要观察三件事。

第一，外部数学家能否独立复核十项结果，并判断每个结果在对应领域中的位置。OpenAI 已经提供论文、Lean 文件和推理记录，复核入口比只有一段自然语言答案的模型演示更完整。

第二，模型提出的路线是否能被人类继续使用。一个偶然找到的证明有价值，但能被概括成方法、推广到相邻问题、进入研究者日常工具箱，价值会更高。十项结果横跨多个领域，后续工作可能集中在不同证明中是否存在可迁移的搜索模式。

第三，归属规则如何落地。模型生成数学论证，人类选择问题、设计提示和验证形式化代码，论文作者、模型和机构的贡献边界需要具体记录。OpenAI 选择把这条生产链写入发布说明，至少让讨论有了可核对的对象。

目前最稳妥的结论，是把这份发布看成十组值得审阅的新数学结果，以及一份关于 AI 参与研究生产线的公开实验记录。Lean 仓库提高了可检查性，论文和推理记录提高了可读性，数学界的独立审阅决定这些结果最终会以什么方式进入学科。

OpenAI论文封面

来源：