OpenAI还有大招！Astra一口气推进10道数学难题，249页论文只是开始

当AI还在比拼考试分数、代码速度时，OpenAI把战场直接推到了人类知识的最前沿。

8月1日，OpenAI发布论文《Ten Advances in Mathematics and Theoretical Computer Science》，公布下一代内部模型Astra在10个长期开放问题上取得的新结果。

问题横跨高维几何、编码理论、群论、算子代数、算术电路复杂度、量子复杂度、格密码学和极值组合学。不是10道竞赛题，也不是已有定理的复述，而是10次向未知边界发起的正面进攻。

这场OpenAI Astra数学突破，很可能会成为AI参与基础科学研究的一张标志性照片。

10个结果，一次打穿8个数学方向

官方清单很硬：

高维球体堆积获得新的渐近上界；

二元码与球面码的经典边界被指数级改进；

构造出明确的非sofic群；

给出Connes刚性猜想反例；

提升永久量的算术电路下界；

证明一般双人量子博弈的指数平行重复定理；

推进最接近向量问题的多项式因子困难性；

解决Ehrhart体积猜想；

改进多色Ramsey数；

并解决两项Erdős极值图论问题。

如果把这些名词翻译成现实语言，它们分别关心：高维空间能塞下多少球、信息怎样编码得更紧、更可靠，哪些无限结构能够被有限模型模拟，计算某类多项式到底需要多少资源，量子玩家把同一场游戏重复很多次后胜率如何变化，以及后量子密码所依赖的格问题究竟有多难。

也就是说，这不是在一个小方向里连续刷题，而是在多个数学大陆同时点亮坐标。

尤其值得注意的是，10项结果的形态并不相同：既有证明一个长期猜想成立，也有构造反例推翻原有判断，还有把已知上界或下界推进到新位置。

能在这三种研究范式之间切换，意味着模型不只会沿着给定路线演算，也开始表现出寻找结构、选择工具和设计构造的能力。

搜索Astra破解十大数学难题，最容易忽略的其实不是数量，而是跨度。

一个模型在同一轮评估中，连续调用调和分析、群表示、概率、傅里叶方法、组合构造和复杂性归约，这种跨领域迁移能力，才是249页文字背后最值得关注的信号。

找到了明确的非sofic群

1999年，阿贝尔奖得主Mikhail Gromov提出sofic群概念。通俗理解，一个无限群如果能用越来越大的有限置换系统逼近其局部乘法结构，就可以称为sofic。

这个框架连接着群论、动力系统、遍历论和算子代数。此后一个核心问题长期悬而未决：所有可数群都是sofic群吗？

可以把它想成一幅无限延展的复杂图案：无论你截取多大一块，都希望找到一张有限缩略图，让局部关系几乎不走样。几十年来，数学家知道很多群都拥有这种可逼近性，却一直缺少一个能被明确抓住的例外。

找到非sofic群，就等于第一次证明：有些无限结构的局部规律，确实无法被有限置换模型完整逼近。

Astra给出的答案，是构造二元Leavitt代数的单位群，并证明它不是sofic群。论文把property-(T)展开子、Kun-Thom中心化子障碍、Thompson群V等工具串到了一条证明链上。

Astra非sofic群证明的精彩之处，不只是给出否，而是把那个此前只存在于数学家想象中的边界，变成了一个可以被明确写下、逐步检查的对象。

改写高维球体堆积的旧边界

怎样把同样大小的球塞得最密？在三维里，它像码橘子；到了高维，它会迅速变成几何学与信息论共同面对的难题。2022年，Maryna Viazovska因解决8维球体堆积等工作获得菲尔兹奖。而当维度趋向无穷，通用上界仍是一块更广阔的版图。

这次高维球体堆积最新突破，精确确定了Cohn-Elkies线性规划上界的指数衰减率，并给出自1978年以来通用球体堆积指数的首次改进。换句话说，Astra不只是为某个特殊维度找到漂亮答案，而是在回答维度不断升高时，最优密度究竟怎样衰减。这也是OpenAI 249页数学论文中最容易让非专业读者直观感受到分量的一章。

Cohn-Elkies方法的妙处，是把几何堆积问题转化为寻找满足特定符号条件的辅助函数，再借助傅里叶变换控制密度。过去，人们知道这套线性规划非常强，却没有精确看清它在超高维极限中的指数能力。Astra给出的结果，相当于不仅把仪表盘上的指针向前推了一格，还把这台仪器能测到哪里说明白了。

给Connes刚性猜想一场反向烟花

1982年菲尔兹奖得主Alain Connes曾提出：在一类具有property-(T)的ICC群中，群生成的冯·诺依曼代数，或许足以像指纹一样确定原来的群。

Astra构造的不是一对偶然撞脸的例子，而是一个可数无限家族：这些群两两不同构，却拥有同构的群冯·诺依曼代数。Connes刚性猜想反例因此呈现出一种非常有力量的结构感：指纹相同、主体不同不是孤例，而可以成族出现。

如果继续用比喻理解，这像是发现无数座外形与内部通道都不同的城市，投射到某种更高层的代数地图上后，却生成同一张地图。反例从一次例外扩展成稳定出现的一族结构，也为研究群与算子代数之间究竟保留了哪些信息，打开了新的入口。

证明、过程和证书同时公开

这轮发布不只有最终结论。OpenAI还公开了62页推演笔记，解释关键想法如何连接；同时在OpenAI ten-proofs GitHub仓库中，放出了10项结果对应的Lean 4证书。

Lean 4形式化验证数学证明的价值，在于把论证翻译成机器可检查的精确定义与推理步骤，让复核者可以从读起来像对的，继续走向由证明助手逐项核验。

传统论文更像一封写给同行的长信，形式化证书则像一份可以运行的逻辑凭证。定义是否一致、条件是否被遗漏、每一步是否真的从前一步推出，都必须在统一的形式系统里落地。

OpenAI还给出了独立检查这些形式化文件的路径，这使论文、思路说明和机器证书形成了三层互相对应的材料。

另一个极具冲击力的数字是成本。OpenAI称，找到这10个解法所消耗的token，按Sol API价格折算约为2000美元。

这里讨论的是成功解法运行的等价成本，而它仍然让AI发现数学定理成本第一次变得如此具体：基础研究中的高强度探索，开始拥有一种可规模化调用的新形态。

平均到每项结果，数字大约是200美元。当然，真正的科研价值不能只按一次推理账单计算；选题、整理手稿、形式化和学术交流仍共同构成完整流程。更重要的变化在于，过去稀缺的高强度试路线能力，如今可以更频繁地被调用，让研究者同时探索更多大胆构想。

因此，这次发布最值得记住的，不是AI要不要取代数学家，而是AI辅助数学研究已经跨过了一个关键门槛：它能在人工智能解决开放数学问题时提出构造、组织长证明、接受形式化核验，并把结果交还给学术共同体继续发展。

今天，我们看到的或许不是数学荣耀的退场，而是它拥有了新的参与者。下一批被打开的，可能是量子平行重复定理，也可能是格密码最接近向量问题，或者某个尚未进入大众视野的猜想。