OpenAI Astra模型花2000美元攻克10道数学难题，但争议随之而来

Astra攻克了哪些难题？

这10项成果横跨了异常广泛的学科领域：高维几何、编码理论、算术电路复杂性、群论、算子代数、量子复杂性、格密码学以及极值组合学 。

1. 高维球体堆积 —— 球体堆积密度的新上界，逼近Cohn–Elkies阈值 。
2. 二元码和球面码 —— 在任何指定最小距离下，对最大码规模的指数级改进界限 。
3. 非sofic群 —— 首次明确构造出非sofic群的存在性，这是群论中的一个核心开放问题 。
4. Connes刚性猜想 —— 推翻了一个关于冯·诺依曼代数的长期猜想 。
5. 算术电路复杂性 —— 计算永久式（Permanent）的新下界，包括一个n⁴/log n阶的公式下界 。
6. 量子并行重复 —— 针对一般双玩家量子博弈的指数级并行重复定理 。
7. 最近向量问题 —— 多项式因子的近似困难性，这是后量子密码学的基础 。
8. Ehrhart体积猜想 —— 确定了质心是其唯一内点格点的凸体的最大可能体积 。
9. 多色拉姆齐数 —— 一个超指数下界，解决了Erdős问题183 。
10. 极值数猜想 —— 在紧致性和退化性猜想上取得成果，解决了Erdős问题146和180 。

验证方法：非Lean不可

OpenAI并未发布Astra模型本身，而是在GitHub上以Apache 2.0许可证发布了Lean 4证明证书，并报告称“sorry”计数为零——这意味着所有十个形式化证明的每一步都得到了完全验证 。这种方式避开了关于AI生成推理是否正确的那种常见争论：证明助手通过机械化方式强制执行正确性，无论论证是如何被发现的。

社区反应：印象深刻，但存在分歧

即便像Noam Brown这样的研究者称之为科学推理的一大步 ，怀疑论者也提出了重大质疑。

不是最顶尖的难题。 多位观察者指出，这10个问题均非克雷数学研究所的千禧年大奖难题（例如P vs. NP、黎曼猜想）。这些问题本身是严肃的开放问题——例如非sofic群的构造自1999年Mikhail Gromov引入sofic概念以来就一直悬而未决 ——但它们并不具备同样的“头条”分量。

未经同行评审。 这些结果由OpenAI直接宣布，并未事先在同行评议的数学期刊或会议论文集上发表 。批评者认为，AI生成的发现与人类辅助的框架之间的界限仍然模糊，OpenAI自身也通过引用《莱顿AI与数学宣言》承认了这种张力 。

泛化能力存疑。 认知科学家Gary Marcus认为，在形式化数学上的成功是一个无法推广到更广泛的科学推理的“特例”，在一个领域的专长并不能保证在所有领域的专长 。数学适合生成廉价、可验证的合成数据，而这在大多数科学领域并不成立。

可重复性担忧。 由于模型未发布且具体的提示方法未完全公开，独立验证整个生成过程是不可能的 。一些批评者关注点在于，没有Astra模型本身，复制这些结果非常困难。

商业时机。 此公告发布之际，正值OpenAI定位其下一个主要模型家族，这引发了关于该研究是为了营销效果而非科学严谨性的质疑 。

这意味着什么

如果这些证明能够经受住专家们的审视，其中几项成果将终结困扰学界数十年的问题。最突出的成就——首次明确构造非sofic群——解决了一个存续超过25年的问题 。即使是批评者也承认，OpenAI提供了比典型的公司公告多得多的可审查材料 。

但更广泛的问题不在于Astra是否能做数学。而是在一个狭窄领域内解决形式化、可验证的问题，是否能转化为通用科学推理能力。答案，目前是：尚未得到证明。