OpenAI 称下一代模型 Astra 推出数学与理论计算机十项进展，Token 成本约 2000 美元

据 IT之家 8 月 1 日消息，OpenAI 官方公布了其在数学与理论计算机科学领域取得的十项进展。来源显示，这些问题此前至少十年以上没有实质性突破，部分问题悬而未决的时间更长。OpenAI 称，相关结果由下一代核心模型 Astra 的内部版本计算得出；如果按 Sol API 费率估算，寻找这些解法所消耗的总 tokens 成本约为 2000 美元。这意味着，前沿基础研究中“模型生成证明、人类验证与整理”的新协作方式，正在被推到更公开的位置。

Astra 涉及的十类进展：覆盖数学、复杂性与密码学基础

从 OpenAI 公布的信息看，这次并非单点式能力展示，而是横跨多个高度抽象的研究方向，包括高维几何、编码理论、群论、算术复杂性、量子复杂性、格问题、凸几何、拉姆齐理论与极值图论等。对普通科技读者来说，这些名称距离日常应用较远，但其中不少问题是信息论、密码学、计算复杂性和算法理论的底层支柱。

• 高维球体堆积：给出了球体堆积密度新的上界，并将界限收紧至 Cohn-Elkies 阈值。
• 二进制与球面码：在给定最小距离下，对二进制码最大规模界限实现指数级改进，并在高维球面码上取得类似结果。
• 非柔性群：提出构造方法，证明非柔性群存在，回应群论中的核心未解问题。
• 康纳斯刚性猜想：证伪某些群可由其冯·诺依曼代数唯一确定的长期猜想。
• 算术电路复杂性：在积和式计算的算术电路与公式下界上给出新结果，其中包括 n4/log n 阶的算术公式下界。
• 量子平行重复：提出适用于通用两方量子博弈的指数级平行重复定理。
• 最近向量问题：确立多项式因子近似困难度，与后量子密码学相关。
• 埃尔哈特体积猜想：在所有维度中确定相关凸体可能拥有的最大体积。
• 多色拉姆齐数：给出多色三角形拉姆齐数的超指数级下界，解决埃尔德什问题 183。
• 极值数猜想：在极值图论中的紧凑性与退化性猜想上取得成果，解决埃尔德什问题 146 和 180。

AI 生成证明，人类负责验证：科研署名与责任被重新讨论

这次信息中最值得关注的，不只是具体数学结论本身，还包括 OpenAI 对研究过程的表述。OpenAI 认为，署名权应当真实反映成果产生的过程：如果一项证明完全由 AI 系统生成，却被描述成人类独立完成，将抹杀 AI 系统的贡献，也会扭曲人类智力劳动的本质。

来源显示，人类研究员参与了论文手稿撰写，并使用 Lean 语言对证明进行形式化验证，同时对正确性负责；但这些数学论证本身均由 OpenAI 系统生成。换言之，这不是简单的“AI 辅助查资料”或“自动补全文本”，而更接近于模型提出关键论证路径，人类研究者承担审稿、形式化验证、表达与责任确认的混合流程。

影响解读：低成本 Token 是否会改变基础研究节奏？

按来源中的估算，寻找这些问题解决方案的 tokens 成本约为 2000 美元。对于基础数学和理论计算机科学而言，这个数字并不等同于真实科研总成本，因为模型训练、基础设施、人类专家验证、论文撰写和形式化证明都需要额外投入。但它依然传递出一个信号：一旦强推理模型具备稳定探索能力，前沿问题的“候选证明搜索”成本可能会被显著压缩。

对 AI 行业而言，Astra 的这类展示也说明大模型竞争正在从聊天、编程、图像生成，进一步进入高阶形式推理场景。数学证明、复杂性理论和密码学相关问题要求模型在长链条推导中保持一致性，不能仅靠语言流畅度取胜。因此，形式化验证工具如 Lean 的参与，可能会成为未来 AI 科研工作流的重要组件：模型负责生成思路，人类与验证系统共同筛选正确结果。

不过，这些成果仍需要学术共同体进一步审视。对于中文科技读者而言，值得关注的不是“AI 是否已经取代数学家”这类简单结论，而是科研生产方式正在发生变化：AI 可能成为可规模化搜索证明空间的工具，人类专家则更集中于问题选择、验证、解释与责任承担。若 OpenAI 披露的结果获得广泛确认，Astra 将成为观察下一代模型科学发现能力的一个重要案例。