OpenAI 下一代 Astra 模型攻克十项数学开放问题，成本仅 2000 美元

OpenAI 公布其下一代主要模型 Astra 的内部版本在高维几何、编码理论、群论、算术电路复杂性、量子复杂性、格密码学和极值组合等领域给出了十项新的研究结果。这些问题的共同特点是核心结论至少十年没有明显进展，多数等待突破的时间更长。

具体成果包括：高维球体堆积的新上界（推进至 Cohn-Elkies 阈值）；二元码与球面码规模的指数级改进；构造出非 sofic 群，从而证明非 sofic 群确实存在；给出 Connes 刚性猜想的反例；推进算术电路计算 permanent 的下界；证明一般双人量子博弈的指数级并行重复定理；证明最近向量问题在多项式近似因子下的计算困难性；确定一类特殊凸体的最大体积（解决 Ehrhart 猜想）；为多色 Ramsey 数建立超指数级下界（解决 Erdős 问题 183）；在极值图论上解决 Erdős 问题 146 和 180。

这些成果并非针对特定题目专门训练，而是来自 Astra 研发期间的开放问题评测。OpenAI 表示，今年 5 月已披露过类似尝试：一款尚未发布的模型生成了对 Erdős 单位距离猜想的反例，并推动了后续研究。

OpenAI 称，完成十项结果所消耗的 token 按 Sol API 价格计算约值 2000 美元。研究流程包括三步：Astra 内部版本搜索解法并生成数学论证；人类研究人员使用同一模型将论证整理成可公开阅读的论文；模型将每项论证转化为 Lean 证明证书，Lean 是交互式定理证明器，可将证明拆解为机器可逐步检查的形式过程。

OpenAI 同步发布了模型对每项解题过程的叙述，但这些内容更接近模型生成的推理说明，不能简单等同于系统运行时完整、原始的内部计算过程。

这一流程意味着大模型在数学领域的角色正在变化：它开始尝试进入真正的研究无人区，提出此前不存在的论证，并接受形式化证明系统的逐步检查。

过去大模型在科研中的应用主要集中于文献检索、代码编写、数据分析和论文润色，很少直接触及论文最核心的原创结论。OpenAI 此次公布的十项成果试图跨过这条边界：模型不再只帮助表达已有想法，而是在开放问题中搜索可能的结构，形成新的数学论证，并用形式化系统检查结果。

OpenAI 最近还宣布推出 ChatGPT for Academic Researchers，计划向 10 万名科学家和数学家免费开放其最强的 ChatGPT 模型，这十项结果可视为该计划的能力展示。

然而，模型给出证明只是第一步。这十项结果能否经受数学共同体的长期审查，能否被进一步简化、推广和纳入现有理论体系，仍需要专业研究者验证。OpenAI 已将尖锐问题摆在数学界面前：当 AI 能独立产生具有研究价值的数学论证，论文作者、贡献归属和科研评价体系应当如何调整？