OpenAI 的下一代模型 Astra 一举解决了十个有数十年历史的数学公开问题

8 月 1 日，OpenAI 发布报告称，其下一代模型（内部代号 Astra，尚未发布）在十个不同的数学公开问题上给出了新结果。（不，它们不是千禧年大奖难题，但仍然意义重大。）

值得注意的是：这些解答不是对问题的渐进式推进，而是确切的解决方案，并已用 Lean 验证。（Lean 是一种编程语言和证明助理，要求将数学论证的每一步都用机器可读的细节明示出来。） 

信息量很大。在本文中，我按领域整理了这些问题，并以高层次方式说明发生了什么、这对数学学科可能意味着什么，以及我们还能从中窥见 Astra 的哪些信息。

这十个问题是什么？

下面按通俗说法列出每个结果，并标注其所属的数学或计算机科学分支。

非 sofic 群

领域： 群论

Astra 给出了一个群的显式构造，这个群无论多么接近都无法被大型有限结构逼近——从而解决了自 1999 年提出 “sofic” 群概念以来一直悬而未决的问题。该构造附带了证明，表明任何有限逼近序列都不可能奏效；证明在 Lean 中形式化，逻辑可由机器检验。

维基百科已更新：

球堆积

领域： 高维几何

问题是：当维数增加时，如何将相同且不重叠的球尽可能致密地堆积在一起。Astra 在高维情形下证明了更紧的密度上界，这是自 1978 年以来对该特定界的首次改进。它并未给出更好的堆积方法——而是收紧了任何未来方法所能达到的极限。

二进制与球面码

领域： 编码理论

纠错码通过将有效消息彼此保持足够远，使得小错误无法将一条消息变成另一条。Astra 证明了在给定最小距离下，此类消息数量的上限可被显著收紧（指数级改进），并给出了在高维球面上分布点的匹配结果。

Connes 的刚性猜想

领域： 算子代数

Alain Connes 猜想：某些群总能从基于它们构造的代数结构（称为冯诺依曼代数）中被唯一重建。Astra 通过构造两类真正不同却产生相同代数的群加以反驳，表明这种重建并非总是一一对应。

算术电路复杂度

领域： 计算复杂性理论

“Permanent”（永恒行列式）是由一个数阵计算得到的单个数值，计算代价高昂。复杂性理论研究者想知道任何方法所需的算术步骤的可能最小数量。Astra 证明了这一最小值新的、更强的下界——这是著名地极难推动的那类结果。

量子并行重复

领域： 量子复杂性理论

经典理论表明：让两个不能通信的参与者并行重复进行多次困难博弈，会使作弊成功的概率呈指数级下降。Astra 证明了即便参与者共享量子纠缠，这一保证仍然成立，将经典的基础性原理扩展到了量子情境。

最近向量问题

领域： 基于格的密码学

给定一个重复的点阵（格）和一个目标位置，该问题要求找出最近的格点——这在高维中被认为非常困难，因此支撑了一些抗量子的加密方案。Astra 证明了即便在特定的多项式因子范围内近似答案，仍是可证明的困难，从而强化了基于其之上的密码学。

Ehrhart 的体积猜想

领域： 离散与凸几何

对于一个凸形体，若其唯一的内部格点恰位于其质心，数学家想知道在任一给定维度中，这样的形体所能拥有的最大体积。Astra 计算出了各维度下的最大体积，完整解决了该猜想。

多色 Ramsey 数

领域： Ramsey 理论 / 组合学

当人数足够多、关系类别足够多时，最终必然能找到三个人在同一类别下两两相连。Astra 证明：随着类别数量增加，所需的最小群体规模增长速度快于任何固定的指数速率，解决了 Erdős 问题 183。

极值数猜想

领域： 极值图论

这一分支研究的是：在规避某些小的禁用模式的前提下，一个网络最多可以拥有多少连接。Astra 在此解决了两条相关猜想（对应 Erdős 问题 146 与 180），精确刻画了此类网络在这些模式变得不可避免之前所能达到的密度上限。

上述每个问题至少已悬而未决十年；其中数个已存在三十年甚至更久，包括理论计算机科学方向上由图灵奖得主涉猎的问题。

等等，反例是“更容易”的证明吗？

我无意唱反调，但我知道这是常见的问题或反应，尤其来自对数学略有了解的人。

人们最常见的批评是：其中若干结果是反例，而非新的普遍理论。这一观点重要之处在于：反例回答的是是/否问题，但本身并不会告诉您模式为何失效，或提供一族相似对象供后续研究；而像分类定理或新技术之类的成果则能打开更多大门。

我认为这种批评一般来说站得住脚，但并不足以一概否定这整批问题。首先，非 sofic 群的结果并非对既有“擦肩而过”构造的小修小补——在长达 27 年无人得出任何构造之后，这是首个同类显式构造，其背后的技术也有望推广以找到其他例子。

其次，其余九个结果中的若干个（包括球堆积上界和最近向量问题的困难性结果）根本不是反例；它们是对现有界的直接改进。 

尚未解决的事项

接下来几天、几周、几个月，随着学界的进一步检视，有几件事值得持续关注：

\n
• 尚无同行评审。 这些结果已用 Lean 验证，并经部分接触到预印本的数学家非正式审阅，但尚未经过期刊的正式审稿流程。 
\n
• 署名仍在协商中。 OpenAI 表示其对论文和 Lean 形式化负有责任，同时将数学论证本身归功于模型。对过程的独立复现（而非对证明的验证）目前很难做到。
\n

这对数学意味着什么

最直接的转变在于数学家可能真正把时间花在什么上。如果一个表述良好的公开问题可以交给模型并在 Lean 中核查，那么瓶颈就从“是否有人能解出”转向“我们是否提出了正确的问题并正确形式化”。提出好问题并判断哪个值得攻坚，本身就是数学家凭经验培养出的真本领。 

同时，关于经费与学术信誉的问题也在酝酿。科研资助、终身教职评审和奖项历来建立在稀缺性之上：这些问题足够难，以至于解出其中一个就能说明解题者的水平。如果 AI 辅助的成果变得常态化，学界需要新的方式区分什么是真正困难、什么只需花几千美元算力即可达成。当然，普通人并不真正理解这些问题；受过正规训练的人懂，这一点不会改变。所以，数学素养比以往更为珍贵。 

外界如何反应

社交媒体上的反应，与其说在质疑证明是否成立，不如说更多聚焦于这些结果能说明什么。

有些人认为真正的故事是速度本身：横跨不相关领域、十个有数十年历史的问题同时落地，快到专家都来不及审阅。一个关于未来的问题是：“我们能跟得上验证的步伐吗？”

也有人反驳称，这未必能说明太多关于 AI 的一般能力。数学是少有的领域之一，模型的工作可以被自动而完全地检验。大多数现实世界问题并没有这种内置的“标准答案”。在这种观点下，这一成就是确凿的，但它或许更多说明了数学尤其适合 AI。

第三种评论思路是：一个正确但尚无人彻底审阅或吸收的证明，并不算真正被理解了，只是被验证了而已。在这种看法中，发现一个定理与理解其意义，是两份不同的工作。

结语

数学家们表示，非 sofic 群的结果看起来是真正的突破：群论中一个存在数十年的公开问题，被一个显式构造所解决，而且相关领域的数学家严肃对待。其余九个结果合在一起，代表了横跨纯数学多个方向的广泛且技术上分量十足的进展。

尚未发生的是较慢的部分：同行评审、搜索过程的复现，以及学界在这些结果之上继续推进。这部分比一篇博文花的时间更长，而正是它将真正告诉我们这次的影响有多大。我们会持续更新。