闻乐 发自 凹非寺

OpenAI又又又又搞数学了。

“下周颁发的菲尔兹奖，可能是最后一个颁发给人类的菲尔兹奖。”

当时Anthropic研究员留下的这句调侃，眼看快被OpenAI兑现了。

OpenAI放出了下一代主力模型Astra内部测试版本的研究成果——

一次性拿下了10项长期悬而未决的数学与理论计算机科学公开难题。

这批课题横跨高维几何、编码理论、群论、算子代数、量子复杂度和极值组合学等领域。

而且本次产出的全部数学证明均通过Lean形式化工具完成机器验证。

OpenAI还同步公开了模型求解每一道问题时完整的推理过程文本，完整留存了AI思考、调整推导路径等细节供数学家复盘。

在成果发布后，不少顶尖学者给出极具分量的评价。

罗格斯大学杰出教授、美国数学学会Alex Kontorovich留了两个惊叹号……

更扎心的是，Astra解决这10道难题一共花了不到2000美元。

好……好吧，数学现在真变成一款点击游戏了？？

十题连斩

曼彻斯特大学数学家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年KL界提出后始终无优化方案。

高维球体堆积简单说就是：在n维空间里，怎么把同样大小的球塞得最密？

2022年，Viazovska因为解出8维和24维的精确堆积密度，拿了菲尔兹奖。

但任意高维的密度上限，从1978年两位苏联数学家给出Kabatiansky–Levenshtein界之后，整整46年寸步难行。

Astra精确算出了Cohn–Elkies线性规划的指数衰减率，首次突破了KL界的限制。

它最初走的路线是全局范数估计，用柯西-施瓦茨不等式硬上。

但很快Astra自己否掉了这条路，理由是全局范数会忘记负质量集中在哪。

于是随即转向了局部质量排除不等式，把问题从实数轴解析延拓到带形区域，利用径向傅里叶变换的梅林反射性质，最终通过调和测度和最大模原理锁定了下界。

只能说，这个自我纠错能力也是……夯。

类似地，在二进制编码和球面编码问题上，Astra给出了指数级的界改进，刷新了经典的MRRW界。

跳出传统一维分析框架激活微小自由度，更新了通信领域纠错码、信号传输的理论上限。

算术电路方向，Astra给出永久值n⁴/log n阶下界，用矩形匹配多项式解决传统推导的计数失效问题，并借助莫比乌斯变换统一处理除法复杂度；

量子层面证明通用双人博弈指数并行重复定理，填补量子并行重复理论空白；

格密码领域完成CVP多项式近似难度证明，后量子加密的安全性，某种程度上就建立在这类问题上。

Astra还一次性解决三道埃尔德什经典开放问题：

针对183号多色拉姆齐数，模型推导出了

超指数下界，通过调色板机制递归拼接图块，搭配饱和矩阵约束边的配色规则，从构造层面杜绝单色三角形生成；

面对146、180号极值图紧致与退化猜想，它采用双模板分层论证，分别管控扩展集分布、转化异常顶点，依托汉明几何熵窗剔除所有低熵无效子阵列；

Astra解题流水线

这些成果背后的解题过程，大致可以拆成四个阶段。

第一步，Astra围绕一个开放问题自主展开推理，生成完整的数学论证和核心证明思路。

第二步，研究人员复用同款Astra辅助梳理文稿，适配数学界阅读、评审、引用的通用标准。

第三步，再由模型把这些证明进一步形式化，转换成Lean证明。

Lean可以把每一个数学步骤都变成计算机能够验证的逻辑表达，只要其中有任何一步推导存在漏洞，都无法通过验证。

这相当于又多了一层审稿机制。

最后，官方同步开放每道难题对应的完整AI推理叙事文本，完整留存模型试错、更换数学工具、自我推翻思路的全过程，方便全球数学家复盘溯源。

不久前，AI教父Hinton预言未来10到20年内，AI可能创造出人类无法理解的新数学。

以Astra今天的表现来看，这样的未来好像真不远了。