继五月用未发布模型推翻 Erdős 单位距离猜想之后,OpenAI 今日一次性公布十项数学与理论计算机科学进展——每一项都解决或大幅推进一个长期悬而未决的开放问题。这些成果覆盖高维几何、编码理论、算术电路复杂度、群论、算子代数、量子复杂度、格密码与极值组合,由下一代模型 Astra 的内部版本完成。
十个问题,一个惊人的成本数字
OpenAI 表示,解决这十个问题所需的总 token 数,按 Sol API 费率计算仅约 2000 美元。论证由 Astra 内部版生成,人类负责整理成稿,模型随后把每个论证在 Lean 证明助手中形式化(仓库已开源:github.com/openai/ten-proofs),并公开每个解法的模型思考叙述。
十个成果包括:高维球堆积密度的新上界(逼近 Cohn–Elkies 阈值);二元码与球码最大尺寸的指数级改进上界;首次构造非 sofic 群(群论核心开放问题);推翻 Connes 刚性猜想;permanent 的算术公式下界达 n⁴/log n;一般双人量子博弈的指数级并行重复定理;最近向量问题(CVP)的多项式因子难近似性(与后量子密码直接相关);Ehrhart 体积猜想;多色三角 Ramsey 数的超指数下界(解决 Erdős 第 183 题);极值图论紧致性与退化猜想(解决 Erdős 第 146、180 题)。
对数学共同体的责任
OpenAI 特别提到莱顿宣言(Leiden declaration on AI and Mathematics)签署方的关切。他们的立场是:归属必须诚实地反映成果的产生方式——把一个完全由 AI 生成的证明署名为人类作者,既歪曲了系统贡献,也歪曲了真正的人类智力劳动。因此 OpenAI 声明:人类协助准备手稿并在 Lean 中形式化证明,并为正确性负责,而数学论证本身由系统生成,希望数学共同体深入审视、把想法带入新的研究。
社区反响
这条 391 分、676 条评论的帖子讨论热度极高。有人兴奋地认为”AI 正在把数学带向主流”,也有人指出关键是速度——两年前我们还远未接近这个状态。围绕”象棋类比”爆发了争论:不少人反感把数学研究比作国际象棋(棋手受限于计时环境,而解决数学问题是有报酬的智力劳动)。还有评论聚焦模型生态:闭源模型遥遥领先,开源模型何时追上,就像 Stockfish 当年追上 AlphaZero 一样。
原文:Ten advances in mathematics and theoretical computer science | HN 讨论:news.ycombinator.com/item?id=49157930