OpenAI再次在数学领域发起了猛攻。此前Anthropic研究员的一句玩笑话——“下周颁发的菲尔兹奖，可能是最后一个颁发给人类的菲尔兹奖”——眼看就要被OpenAI兑现了。OpenAI发布了其下一代主力模型Astra的内部测试研究成果，一举攻克了10项长期悬而未决的数学与理论计算机科学公开难题。这些课题横跨高维几何、编码理论、群论、算子代数、量子复杂度及极值组合学等多个前沿领域。更令人惊叹的是，所有数学证明均通过Lean形式化工具完成了机器验证。OpenAI还同步公开了模型求解每一道难题时的完整推理过程文本，详细留存了AI思考、调整推导路径等细节，供全球数学家复盘。成果发布后，不少顶尖学者给出了极具分量的评价。罗格斯大学杰出教授、美国数学学会的Alex Kontorovich就留下了两个惊叹号。更令人咋舌的是，Astra解决这10道难题的总成本还不到2000美元。看来，数学如今真的变成了一款点击游戏了？？
01、十题连斩
曼彻斯特大学的数学家Thomas Bloom认为，本次集中发布的十项结论，整体学术价值远超五个月前OpenAI证伪埃尔德什单位距离猜想的单次成果。其中，非sofic群存在性构造被不少数学家视为此次最重磅的成果，具备冲击数学顶尖奖项的水准。加州理工的一位数学博士曾表示，非sofic群问题“这就是菲尔兹奖级别的东西”。1999年，阿贝尔奖得主Mikhail Gromov提出sofic群概念，核心问题极其简洁：所有可数群都是sofic的吗？换句话说，任何无限复杂的群能否用有限置换去逼近它的局部乘法表？这个问题牵动着sofic熵理论、动力系统遍历论和算子代数一整片数学版图。27年间无数顶尖数学家尝试构造反例，全部折戟。Astra则从数学工具箱中直接拎出了二元Leavitt代数的单位群，将Kun-Thom扩展图理论和Thompson群V糅合在一起，逼出了一个决定性的矛盾。在推理过程中，Astra起初尝试随机化网格论证，发现走不通，随即果断放弃，转向了确定性的中位数论证。
同一赛道上的另一大成果，是1982年菲尔兹奖得主Alain Connes的刚性猜想被直接证伪。Connes曾断言某些群由它们的von Neumann代数唯一决定。Astra构造了一个可数无限的群族：这些群彼此之间互不同构，结构完全不同，但它们的von Neumann代数却完完全全相同。整个构造的核心，在于Astra主动区分了两种容易混淆的共轭关系：可测共轭和代数共轭。这个区分一旦建立，后续的构造便水到渠成。Astra在一个二次布尔模上定义了进位等变闭链，分别利用线性群律和二次群律造出了两个不同构却代数不可区分的群。
此外，停滞了46年的高维球体堆积研究也取得突破。自1978年Kabatiansky–Levenshtein界提出后，任意高维球体的密度上限始终无优化方案。虽然2022年Viazovska因解出8维和24维的精确堆积密度获得菲尔兹奖，但高维上限的难题困扰了数学界半个世纪。Astra精确算出了Cohn–Elkies线性规划的指数衰减率，首次突破了KL界的限制。最初它试图通过全局范数估计（利用柯西-施瓦茨不等式）硬上，但很快发现此路不通，因为全局范数会忽略负质量集中的位置。于是它迅速转向局部质量排除不等式，将问题从实数轴解析延拓到带形区域，利用径向傅里叶变换的梅林反射性质，最终通过调和测度和最大模原理锁定了下界。这种自我纠错能力着实令人惊叹。
类似地，在二进制编码和球面编码问题上，Astra给出了指数级的界改进，刷新了经典的MRRW界。这跳出了传统一维分析框架，激活了微小自由度，更新了通信领域纠错码和信号传输的理论上限。在算术电路方向，Astra给出了永久值$O(n^4/log n)$的下界，利用矩形匹配多项式解决了传统推导的计数失效问题，并借助莫比乌斯变换统一处理除法复杂度；量子层面则证明了通用双人博弈指数并行重复定理，填补了量子并行重复理论的空白；格密码领域完成了CVP多项式近似难度证明，这直接关系到后量子加密的安全性。
Astra还一次性解决了三道埃尔德什经典开放问题：针对183号多色拉姆齐数，模型推导出了超指数下界，通过调色板机制递归拼接图块，搭配饱和矩阵约束边的配色规则，从构造层面杜绝了单色三角形的生成；面对146、180号极值图紧致与退化猜想，它采用双模板分层论证，分别管控扩展集分布、转化异常顶点，依托汉明几何熵窗剔除了所有低熵无效子阵列。
02、Astra解题流水线
这些成果背后的解题过程，大致可以拆解为四个阶段。第一步，Astra围绕一个开放问题自主展开推理，生成完整的数学论证和核心证明思路。第二步，研究人员复用同款Astra辅助梳理文稿，使其适配数学界阅读、评审、引用的通用标准。第三步，再由模型把这些证明进一步形式化，转换成Lean证明。Lean可以将每一个数学步骤都变成计算机能够验证的逻辑表达，只要推导中存在任何漏洞，都无法通过验证。这相当于又多了一层严苛的审稿机制。最后，官方同步开放每道难题对应的完整AI推理叙事文本，完整留存模型试错、更换数学工具、自我推翻思路的全过程，方便全球数学家复盘溯源。
不久前，AI教父Hinton预言，未来10到20年内，AI可能创造出人类无法理解的新数学。以Astra今天的表现来看，这样的未来似乎真的不远了。