摘要：OpenAI内部版本Astra公布十项数学与理论计算机科学新结果，并同步交付论文、发现过程说明和Lean 4形式化证书。真正值得关注的不是“AI解出十道题”，而是一套人类选题、模型探索、形式系统验证、专家判断意义的科研生产流程正在形成。
2026年8月1日，OpenAI公布了一组颇具冲击力的研究成果：其下一代模型Astra的内部版本，在高维几何、编码理论、群论、算术复杂性、量子计算、格密码学和极值组合等领域，给出了十项新的数学与理论计算机科学结果。
这次发布包含一份249页的论文合集、一份62页的发现过程说明，以及可以公开运行的Lean 4形式化证明仓库。OpenAI称，这些问题的主要结论至少十年没有取得实质进展，多数问题停滞时间更长。十项结果的核心数学论证由Astra生成，人类研究人员使用同一模型将论证整理成论文，随后由模型把证明转换为Lean证书。
如果十项结果经过数学共同体的持续检查后仍然成立，这次发布的意义将远远超过一次模型能力展示。它呈现出一套正在成形的科研生产流程：人类选择重要问题，模型进行长时间探索，形式化系统负责逐步验算，领域专家判断结果的意义、适用范围和后续方向。
十项结果究竟解决了什么
OpenAI公布的十项成果横跨多个彼此距离很远的学科。从研究内容看，大致可以分为高维几何与编码、代数与算子理论、计算复杂性与量子计算、极值组合四组。
1. 高维球体堆积：改写持续近半个世纪的指数界
球体堆积研究在给定维度中，形状相同的球最多能够占据多大空间比例。三维情形对应著名的开普勒猜想；在八维和二十四维，Viazovska等人借助傅里叶分析找到了最优结构。但随着维度升高，球体堆积密度会迅速衰减，其精确衰减速度长期缺少答案。
Astra给出的结果确定了Cohn—Elkies傅里叶线性规划方法在高维极限下的精确指数：
$$\lim_{d\to\infty}LP_d^{1/d}=\sqrt{\frac{e}{2\pi}}$$
将其写成更直观的二进制指数形式，相应密度上界约为：
$$\Delta_d\leq 2^{-(0.6044\ldots+o(1))d}$$
1978年以来，高维球体堆积的一般上界主要停留在Kabatianskii—Levenshtein给出的0.59905576指数。新结果将其提高到约0.6044。数值差距看起来只有千分之几，但在指数中，维度越高，差距就会被指数级放大。论文将其称为1978年以来一般球体堆积指数的首次改进。
这项证明还确定了相关傅里叶符号不确定性问题的渐近常数：正、负傅里叶特征函数的临界半径都趋近于
$$\frac{\sqrt d}{\pi}$$
证明的关键路径，是把高维几何问题转化为傅里叶线性规划，再利用径向傅里叶变换、Mellin变换和符号不确定性建立精确渐近界。
2. 二进制码和球面码：在所有距离参数上获得指数改进
编码理论研究如何在有限空间中安排尽可能多的码字，同时保证任意两个码字之间具有足够大的距离。距离越大，抗噪和纠错能力通常越强，但可容纳的码字数量也会减少。
Astra建立了一组新的层级式界，对固定最小距离下的二进制码数量给出指数级更强的上界，并将相似方法扩展到球面码。论文强调，这种改进覆盖所有允许的距离参数，而非只在某个狭窄区域有效。
其技术思路没有局限在寻找一个更好的单一多项式，而是构造一套逐层增强的表示论和线性规划层级。对于球面码，当距离参数趋向适当极限时，这套结果还能重新导出前述高维球体堆积指数，说明两个问题在深层结构上存在统一性。
3. 非索菲克群：回答“所有群能否被有限系统近似”
索菲克群可以粗略理解为能够用有限置换系统进行近似的无限群。大量常见群都属于索菲克群，但“是否每一个可数群都是索菲克群”长期没有答案。
Astra构造了一个明确的非索菲克群，从而给出了否定答案。根据论文和发现过程说明，这项构造把具有性质（T）的扩张图、二进制Leavitt代数、自相似结构以及Thompson群的某些性质组合到一起，使任何有限置换近似最终都会遭遇无法同时满足的约束。
这类问题的困难集中在构造。证明某个对象不存在，可以从抽象矛盾入手；给出一个具体反例，还需要设计对象、证明它具有所需性质，并排除所有可能的有限近似方式。Astra的发现笔记记录了从“寻找有限近似中的障碍”到“利用扩张图集中性制造统一矛盾”的探索路径。
4. Connes刚性猜想：同一个算子代数可以对应不同的群
群冯·诺依曼代数会把离散群转化为算子代数对象。Connes刚性猜想关注一个非常基础的问题：对于具有性质（T）的群，其群冯·诺依曼代数是否足以唯一确定原来的群。
Astra构造了无穷多个两两不同构的性质（T）群，但它们的群冯·诺依曼代数彼此同构，由此否定了相关刚性猜想，同时回答了Popa提出的一个有限对一问题。
从信息压缩的角度看，这项结果说明，从群到算子代数的映射会丢失比此前预期更多的信息。即便限定在刚性很强的性质（T）群中，算子代数仍可能无法还原最初的群结构。
5. Permanent计算复杂性：突破长期停滞的无条件下界
一个 $n\times n$ 矩阵的Permanent与行列式形式相似：
$$\operatorname{per}(X)=\sum_{\sigma\in S_n}\prod_{i=1}^{n}x_{i,\sigma(i)}$$
行列式在每一项前带有正负号，Permanent则全部相加。这个看似简单的差异，造成了巨大的复杂性鸿沟：行列式可以高效计算，Permanent是代数复杂性理论中的核心困难对象。
Astra给出了两个新的无条件下界：
- 无除法算术电路计算Permanent至少需要
$$\Omega(n^2\log\log n)$$
个算术门；
- 算术公式计算Permanent至少需要
$$\Omega\left(\frac{n^4}{\log n}\right)$$
个变量叶节点；即便公式允许除法，只要每个分母都是非零有理函数，仍保持同阶下界。
此前，任意深度无除法电路最直接的下界大致是输入规模对应的 $\Omega(n^2)$，经典的一般公式下界约为 $\Omega(n^3)$。新结果分别加入了 $\log\log n$ 因子，并把公式下界推进到接近四次方。
电路部分使用了临界轨迹、梯度映射、Bézout型次数界，以及单位根消去构造；公式部分则利用匹配系数的代数独立性，把大量独立系数需求分摊到互不重叠的变量匹配上。这些方法还解释了为什么同样的证明不能直接用于行列式。
需要强调的是，这项结果仍未解决“Permanent是否需要超多项式规模的一般算术电路”这一终极问题，但它在一个极难取得无条件进展的领域中推进了已知边界。
6. 量子并行重复：重复游戏的获胜概率指数下降
在经典复杂性理论中，如果玩家参加一个单轮获胜率低于1的游戏，并被要求同时赢下多轮独立游戏，那么全部获胜的概率通常会随轮数指数下降。这被称为并行重复现象。
量子纠缠让问题复杂得多。多个并行游戏之间可以通过纠缠策略产生关联，因此经典证明不能直接搬用。此前研究只对锚定游戏等特殊类型获得指数下降，对一般双人量子游戏只知道较弱结果。
Astra证明，对任意有限、双人、单轮量子游戏，只要单局最优纠缠获胜概率为
$$\omega^*(G)=1-\varepsilon<1$$
那么并行进行 $n$ 次并要求全部获胜时，其概率满足指数衰减界。论文给出的形式大致为：
$$\omega^*(G^{\otimes n}) \leq \exp\left( -c\frac{\varepsilon^{13}} {\varepsilon+\log(|A||B|)}n \right)$$
其中 $A$、$B$ 是两名玩家的答案集合，$c$ 为普适正常数。
这项结果把经典复杂性理论中的基础原则扩展到一般量子纠缠游戏，对量子交互证明、非定域性研究和量子密码协议分析都有意义。
7. 最近向量问题：得到 $n^{1/400}$ 近似困难性
最近向量问题CVP要求：给定一个格和目标点，找出格中距离目标点最近的向量。格问题是后量子密码的重要数学基础，许多密码方案的安全性都与其计算困难性有关。
Astra从3SAT构造了确定性多项式时间归约，证明欧氏最近向量问题在
$$n^{1/400}$$
近似因子下仍然困难。其构造利用特征为2的有限域、Reed—Solomon幂和约束、Hankel型重构以及奇偶提升格，把布尔变量赋值和子句满足关系编码进格距离。
这项结论属于最坏情况下的复杂性下界：欧氏GapCVP在格秩为 $n$、近似因子为 $n^{1/400}$ 时仍是NP-hard，除非P=NP，否则不存在解决所有实例的确定性多项式时间算法。它并不意味着现有格密码体系被攻破，也不能直接等同于某个具体密码方案的安全证明，而是推进了对相关格问题复杂性边界的理解。
8. Ehrhart体积猜想：证明所有维度下的精确上界
Ehrhart体积猜想讨论一类特殊凸体：其重心是内部唯一的格点。猜想认为，$n$维凸体的体积满足精确上界
$$\operatorname{vol}(K)\leq\frac{(n+1)^n}{n!}$$
Astra给出了适用于所有维度的证明。其发现过程曾尝试调和对称化等路线，最终转向复几何和代数几何语言，为一般凸体构造环面势函数，结合Bergman核、凸性和复球收缩得到上下斜率估计，补上了猜想中长期缺失的阶乘因子。
这项工作体现了模型进行跨领域方法迁移的能力：一个凸几何和格点计数问题，最终借助复几何工具得到解决。
9. 多色Ramsey数：给出超指数下界
多色三角形Ramsey数 $R_k(3)$ 询问：对完全图的边使用 $k$ 种颜色染色，至少需要多少个顶点，才能保证出现某种颜色的单色三角形。
Astra证明：
$$R_k(3)=k^{\Theta(k)}$$
这给出了超指数下界，解决了Erdős问题183；再结合此前已有的阶乘型上界，可以确定 $R_k(3)=k^{\Theta(k)}$ 的粗增长量级。证明通过构造相互分离的颜色调色板、设计递归的跨边染色规则，以及控制异常颜色模式，使每次递归都能获得随 $k$ 增长的基数提升。
Ramsey理论中的此类结果经常面临“局部避免结构容易、全局同时避免极难”的矛盾。新构造提供了能够跨尺度保持无单色三角形性质的组合机制。
10. 极值图论：否定两个长期猜想
最后一组结果分别否定了Erdős—Simonovits紧致性猜想和Erdős提出的一个退化度猜想，对应Erdős问题146和180。
紧致性结果使用围长为8的几何结构、半平方图和广义四边形构造反例；退化度结果则在Hamming型宿主图中引入熵势函数，通过稀疏化排除低熵嵌入，同时保留足够多的边。
这两个问题都属于极值图论：研究在禁止某些子图的条件下，一个大图最多能够保留多少条边。Astra给出的结论表明，若干看起来合理的局部结构推断无法推广到全局极限。
Astra是怎样完成这些研究的
从公开材料看，这次工作的流程可以拆成四个阶段。
第一阶段是问题选择。OpenAI在模型研发过程中，持续使用尚未解决的研究问题评估模型。入选的十个问题都具有清楚的数学陈述、长期研究背景和可判断的结果边界。问题本身由人类研究团队选择，领域文献、定义和已有结论也构成模型探索的基础。
第二阶段是论证搜索。Astra围绕每个问题提出可能的构造、归约、辅助引理和证明路径，并在失败后调整方向。OpenAI公布的62页《How the Ideas Came Together》并非原始逐Token思维记录，而是模型根据探索材料和最终论文整理的发现过程说明。它重点记录曾经尝试过的路线、遇到的障碍、视角切换以及最后的关键构造。
第三阶段是论文整理。OpenAI明确表示，数学论证由模型生成，人类研究人员与模型共同把论证整理为可供数学家阅读的论文。最终论文合集共249页，其中既有定理、定义和证明，也有与经典结果的比较和参考文献。
第四阶段是形式化验证。模型将十项结果写成Lean 4代码，使证明可以由计算机内核逐步检查。
OpenAI还给出了一个引人关注的成本数字：发现这些解法所使用的Token，如果按照Sol API价格计算，合计约为2000美元。这个数字描述的是模型推理Token的价格换算，没有包含问题筛选、模型训练、计算基础设施、人类研究人员时间、论文整理和形式化工程等完整成本。因此，它适合用于衡量一次成熟模型研究搜索的边际推理费用，不宜直接理解为十项研究的全部研发成本。
Lean证书能够证明什么
Lean是一种基于依赖类型理论的交互式定理证明器。数学家需要把自然语言中的对象、假设和结论转换成严格的形式定义，再把证明拆解成Lean能够检查的步骤。Lean内核最终验证：在给定公理、定义和已有定理的前提下，目标结论是否可以被逻辑地推导出来。
OpenAI公开的ten-proofs仓库分别提供了球体堆积、编码理论、非索菲克群、Connes刚性、Permanent、量子并行重复、CVP、Ehrhart体积、Ramsey数和极值图论的Lean文件。项目使用Lean 4.32.0、mathlib和Lake构建系统，主证明项目元数据标注的 sorry_count 为0。研究者可以运行：
1 | lake exe cache get |
检查全部形式化证明，也可以单独构建某个模块。仓库还提供Comparator独立检查说明，用于降低对单一证明环境和构建流程的依赖。
Lean证书显著提高了证明的可核查性。数百页论文中隐藏一个符号错误、遗漏一种边界情况或错误引用某条引理并不少见；形式化系统要求每一步都拥有明确类型和合法依据，可以排除大量低级错误和逻辑跳步。
不过，Lean的通过仍然需要配合领域审查。专家还要判断：
- 形式化定理是否准确表达了原来的开放问题；
- 引入的定义和假设是否与数学共同体使用的版本等价；
- 证明是否依赖过强的前提；
- 自然语言论文与Lean代码之间是否保持一致；
- 结果在相关学科中的新颖性和重要性处于什么位置。
因此，Lean主要回答“形式系统中的推导是否成立”，数学共同体还要回答“这个形式化命题是否覆盖了我们关心的问题”。当前仓库提供了公开构建和Comparator复核流程，但这不能替代独立同行评审，也不意味着十项结果已经获得数学共同体确认。
这次发布透露出的四个技术变化
第一，模型正在从解答已有题目进入开放问题搜索。
数学竞赛题、教材习题和已有定理复现都有标准答案，可用于训练和评测。开放问题没有现成解法，模型需要提出新构造、发现中间引理、识别失败路线，并在较长推理链中保持目标一致性。十项成果如果经受住检查，意味着前沿模型的有效工作时长和探索深度已经明显提高。
第二，跨学科迁移能力开始产生研究价值。
十项问题来自傅里叶分析、表示论、群论、算子代数、代数复杂性、量子信息、格理论、复几何和组合数学。单个模型能够在这些方向之间迁移工具，说明其知识组织方式已开始支持跨领域搜索。例如Ehrhart体积问题最终借助复几何，球体堆积与编码理论通过统一层级结构连接起来，Permanent下界则综合代数几何、匹配结构和电路复杂性。
第三，形式化证明正在成为科研模型的重要输出接口。
自然语言生成速度很快，但验证成本可能很高。模型一次生成十篇复杂论文，会把大量审查压力转移给数学家。Lean把部分审查工作转化为可重复运行的计算过程，使“批量发现”与“批量验证”能够在同一技术流程中衔接。
第四，科研搜索的边际成本可能快速下降。
约2000美元的Token价格换算显示，一旦模型、问题库、工具环境和验证系统建立起来，增加一次新的研究搜索，其推理成本可能远低于传统科研项目的总投入。未来的主要稀缺资源会更多集中在高价值问题选择、可信数据与文献组织、形式化表达、实验设计以及领域判断上。
仍需关注的几个问题
当前公开信息没有给出Astra尝试过多少问题、失败了多少次，也没有披露每项成果的搜索轮数和Token分布。十项成果属于筛选后的成功样本，暂时无法据此计算模型解决开放问题的总体成功率。
Astra目前还是内部模型，外部研究者无法使用相同模型、提示词和搜索预算复现发现过程。已公开的发现笔记属于事后重构材料，也不能完全替代原始运行轨迹。
此外，数学成果的影响力需要时间沉淀。一项证明可以在逻辑上成立，但可能使用已知工具的巧妙组合；也可能提出一种能够影响多个方向的新方法。两者都有研究价值，学术地位却并不相同。接下来，相关领域专家会逐项检查证明、寻找更短的论证、分析方法的推广性，并判断这些结果在学科发展中的位置。
结语：科研模型的评价标准正在变化
过去评价大模型，常用的是考试分数、代码基准、数学竞赛成绩和回答准确率。Astra这次提交的是一组可以阅读、运行、检查和继续发展的研究对象：249页论文、62页发现笔记、十套Lean形式化证书，以及覆盖多个理论领域的新结论。
这套发布方式给科研AI提出了更高标准。模型需要产生新结果，也要给出清楚的论证；需要提供自然语言解释，也要尽可能转化为机器可检查的证书；需要展示成功案例，也应逐步披露搜索成本、失败样本和复现条件。
如果未来模型能够稳定完成这一闭环，科研活动的组织方式会发生明显变化。人类研究者将投入更多精力选择问题、建立概念框架、设计验证体系和解释科学意义，模型则承担大规模文献联结、候选构造搜索、细节推导和形式化工作。
Astra的十项结果是否都会成为经得住时间检验的重要成果，还需要数学共同体逐项判断。但有一点已经十分清楚：AI参与数学研究的方式，正在从偶尔提供灵感，走向能够交付成体系、可验证的研究成果。