OpenAI下一代模型Astra首秀：十个卡了十年的数学问题

OpenAI下一代大模型有名字了，叫Astra，而它的首秀不是聊天演示，是数学。8月1日OpenAI发布了十项数学和理论计算机科学的进展，每个问题的主结果都至少十年没动过。内部版Astra生成论证，人类数学家整理成论文，全部用Lean形式化——证明是机器可验证的，不需要"相信模型"。清单里有高维球堆积密度的新上界（推到Cohn-Elkies阈值）、非sofic群的构造、最近向量问题的多项式因子近似难度（这条连着后量子密码），还有Ehrhart猜想、多色Ramsey数，顺手解决了Erdos第183号问题。

最扎眼的数字：OpenAI说找到这十个解的全部模型用量，按GPT-5.6 Sol的API价格算大约2000美元。两千美元，买走了数学界搁置十年的十个结果。你可以不信大厂的benchmark，但Lean证书这种收据没法造假，而且整套东西全公开了：249页论证、62页发现过程笔记、一个机器可验证的证明仓库。正式同行评审还没走完，论文成稿也有真人深度参与，所以"AI独立解决数学难题"是夸大；但"AI找到关键想法、人类负责写下来"，这本来就是顶尖数学家之间合作的样子。

放到大背景里这事更大。有报道说Astra是一个为多agent协作设计的模型家族，能让一群agent在同一个问题上连续跑几小时甚至几天，Altman已经拿着它给政策制定者做演示。所以这次发布是个卡位动作：模型还没上线，OpenAI就要让"发现新数学"成为它的第一印象——跟Anthropic一直在推的Claude自主科研成果对着打。前沿竞争正在从"回答问题"转向"生产新知识"，谁先把这件事坐实，谁就拿走叙事权。

公告：https://openai.com/index/ten-advances-in-mathematics/ ，Simon Willison的笔记：https://simonwillison.net/2026/Aug/1/ten-advances-in-mathematics/