8月1日，OpenAI 发了一篇标题很学术的博客《数学与理论计算机科学的十项进展》。真正让数学圈坐不住的，是里面第一次点名了他们下一代主力模型 Astra。这个还没正式发布的内部版本，一口气解出了十个在数学和理论计算机科学里挂了至少十年、有的甚至四十年没动静的开放问题。
把证明交给机器去验证
每个论证先由人类研究员用同一个模型整理成能读的手稿，再被模型自己翻译成 Lean 的形式化证明证书。也就是说，结论不是写在论文里让人拍脑袋信，而是拆成机器能一步步检查的推导。所有证明都放在 GitHub 的 openai/ten-proofs 仓库里，Lean 证书一条没漏。
OpenAI 在博客里写明：把一个完全由 AI 生成的证明署名为人类工作，会同时歪曲系统的贡献和真正的人类智力劳动。
这些问题到底有多”老”
随便挑几个就够吓人。高维球体堆积密度的新上界，把这一方向自 1978 年以来的记录往前推了一步；群论里”是否存在非 sofic 群”的疑问，从 1999 年提出就没人答上来，这次被构造出了反例；还有 1980 年 Connes 刚性猜想，也被直接推翻。组合学这边更是顺手解决了好几个 Erdős 老问题。
- 高维球堆积：推进到 Cohn–Elkies 阈值，48 年来首次改进
- 非 sofic 群：构造出首个明确反例，回应 1999 年的核心开放问题
- Connes 刚性猜想：给出反例，涉及由冯·诺依曼代数决定的群结构
- 积和式算术电路下界、量子博弈并行重复、最近向量问题近似困难性
2000 美元意味着什么
OpenAI 算了一笔账：按 Sol API 的费率，找出这些解所需的 token 总成本大约 2000 美元。Noam Brown 随后在 X 上补充，实际成本比这还低，但也坦言团队试过其他更难的题没做出来，离千禧年大奖问题还远。Astra 被描述成面向长周期、多智能体协作的架构——让不同的 AI agent 在几个小时甚至几天里分工啃同一个大问题，而不是对单条提示词秒回。
这件事最让人心里打鼓的地方，是科研流程里”提答案”和”验答案”第一次可能被同一个系统大规模接管。陶哲轩之前就说过，数学正从”证明稀缺”走向”证明过剩”，真正值钱的会变成判断哪些问题值得做、哪些机器思想能长成新方向。OpenAI 也专门提到他们尊重《莱顿宣言》里对署名和同行评审的担忧——能力跑得太快，规矩得跟上。
发表回复