OpenAI下一代Astra亮相：10项开放新突破，成本仅2000美元

一道困扰学界几十年的开放问题，需要多少成本才能取得关键突破？

OpenAI 给出的答案是，十道题加起来，约 2000 美元。

昨天下午，OpenAI 公布了一份颇为惊人的成绩单。其下一代主要模型 Astra 的内部版本，在高维几何、编码理论、群论、算术电路复杂性、量子复杂性、格密码学和极值组合等领域，给出了十项新的研究结果。

其中一些问题至少十年没有取得核心进展，另一些已经悬而未决数十年。结果包括构造出非 sofic 群、推翻 Connes 刚性猜想、解决三个 Erdős 问题，以及推进与后量子密码学密切相关的最近向量问题。

更值得注意的是，OpenAI 称，这些论证由 Astra 生成。人类研究人员随后借助同一个模型将论证整理成论文，模型又把每项证明形式化为 Lean 证书。按照 Sol API 的价格计算，模型寻找全部解法所消耗的 token，成本大约为 2000 美元。

OpenAI 研究科学家、o1、o3 系列关键研究领导者之一 Noam Brown

这意味着，大模型在数学领域扮演的角色正在发生变化。它开始尝试进入真正的研究无人区，提出此前不存在的论证，并接受形式化证明系统的逐步检查。

当然，模型给出证明只是第一步。这十项结果究竟能否经受数学共同体的长期审查，能否被进一步简化、推广和纳入现有理论体系，仍需要专业研究者验证。

但 OpenAI 已经将一个更尖锐的问题摆在数学界面前：当 AI 能够独立产生具有研究价值的数学论证，论文作者、贡献归属和科研评价体系应当如何调整？

一款尚未发布的模型，挑战十个长期开放问题

这些数学成果来自 Astra 模型研发期间的开放问题评测，并非专门训练一个系统解决某一道特定题目。

今年 5 月，OpenAI 已经披露过一次类似尝试。当时，一款尚未发布的模型生成了对 Erdős 单位距离猜想的反例。OpenAI 表示，这项工作此后推动了数学和理论计算机科学领域的多项后续研究。

这一次，OpenAI 将范围扩大到了十个问题。它们的共同特点是，核心结论至少十年没有明显进展，多数问题等待突破的时间更长。

1 高维球体堆积

模型给出了新的球体堆积密度上界，将现有结果推进至 Cohn–Elkies 阈值。

球体堆积研究的是，如何在给定空间中放入尽可能多、彼此不重叠的球。它既是几何学中的经典问题，也与编码理论、信息论等领域存在紧密联系。

2 二元码与球面码

对于任意给定的最小距离，模型指数级改进了二元码最大规模的已知界，并在高维球面码问题上得到类似结果。

编码理论中的核心问题之一，是在保证不同编码之间具有足够距离的前提下，尽可能增加可用编码的数量。这直接关系到通信系统的抗噪能力。

3 非 sofic 群

模型构造出一个非 sofic 群，从而证明非 sofic 群确实存在。

sofic 群由 Gromov 提出。长期以来，数学家一直不知道所有群是否都是 sofic 群。OpenAI 将这项结果描述为对群论一个核心开放问题的解决。

4 Connes 刚性猜想

模型给出了 Connes 刚性猜想的反例。

该猜想涉及群与冯・诺依曼代数之间的关系，大致关注某些群能否由其对应的冯・诺依曼代数唯一确定。Astra 的结果表明，这种唯一性并不总是成立。

5 算术电路复杂性

6 量子并行重复

模型证明了适用于一般双人量子博弈的指数级并行重复定理。

在经典复杂性理论中，并行重复意味着多次同时执行一个博弈后，作弊者成功通过全部测试的概率会迅速下降。将这一原则推广到量子环境，长期以来面临纠缠策略等额外困难。

7 最近向量问题

模型证明了最近向量问题在多项式近似因子下的计算困难性。

最近向量问题要求在一个格中找到距离目标点最近的格点。它是格理论中的基础问题，也与后量子密码学的安全性密切相关。

8 Ehrhart 体积猜想

模型确定了任意维度下，一类特殊凸体所能达到的最大体积。

这类凸体的质心是其内部唯一的格点。该结果解决了 Ehrhart 提出的一个长期猜想。

9 多色 Ramsey 数

模型为多色三角形 Ramsey 数建立了超指数级下界，并由此解决 Erdős 问题 183。

Ramsey 理论研究的是，当一个系统足够大时，某种有序结构必然出现。多色 Ramsey 数则进一步考察使用多种颜色对图的边进行染色时，单色结构出现的临界规模。

10 极值数猜想

模型在极值图论的紧致性猜想和退化性猜想上取得结果，解决了 Erdős 问题 146 和 180。

从生成论证到 Lean 形式化

这次公布的成果包含一套较为完整的研究流程。

首先，Astra 内部版本搜索开放问题的解法，并生成数学论证。OpenAI 表示，完成十项结果所消耗的 token，按照 Sol API 价格计算约值 2000 美元。

随后，人类研究人员使用同一模型，将原始论证整理成可以公开阅读的论文。

最后，模型把每一项论证转化为 Lean 证明证书。Lean 是一种交互式定理证明器，可以把证明拆解为机器能够逐步检查的形式过程。与自然语言论文相比，形式化证明能够减少论证中隐藏跳步、歧义和逻辑漏洞的空间。

OpenAI 还同步发布了模型对每项解题过程的叙述。不过，这些内容更接近模型生成的推理说明，不能简单等同于系统运行时完整、原始的内部计算过程。

论文地址：https://cdn.openai.com/pdf/ten-proofs-oai.pdf

AI 正在深入科研探索

过去，大模型在科研中的应用主要集中于文献检索、代码编写、数据分析和论文润色。这些工作能够提高研究效率，却很少直接触及一篇论文最核心的原创结论。

OpenAI 此次公布的十项成果试图跨过这条边界。

模型不再只帮助研究人员表达一个已经存在的想法。它开始在开放问题中搜索可能的结构，形成新的数学论证，并用形式化系统检查结果。科研流程中的「提出答案」与「验证答案」，第一次有可能同时被模型大规模介入。

OpenAI 最近还宣布推出 ChatGPT for Academic Researchers，计划向 10 万名科学家和数学家免费开放其最强的 ChatGPT 模型。公司希望让更多研究人员使用 AI 加速科学发现。

这十项结果，可以看作 OpenAI 为这一计划提供的一次能力展示。

真正重要的变化或许还在后面。当提出猜想、寻找证明、检查逻辑和形式化验证逐步连接起来，数学研究的瓶颈可能发生转移。研究者需要花费更多精力判断哪些问题值得解决，哪些机器生成的思想具有更深层的理论意义，以及如何将一段正确的证明发展成新的数学方向。

博客地址：https://openai.com/index/ten-advances-in-mathematics/