
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 也专门提到他们尊重《莱顿宣言》里对署名和同行评审的担忧——能力跑得太快,规矩得跟上。








