最重要的数字是 460,000：OpenAI 于 8 月 1 日向一个公开 GitHub 仓库上传的可机器检验证明的行数，用以支撑其在数学和理论计算机科学领域自称的十项进展。宣布这些进展的博客文章日期同为当天早上，称成果来自 Astra 的一个内部版本，即'我们的下一代主力模型'。十项成果各附一份 Lean 证书，即可机器检验的形式化证明，放在 github.com/openai/ten-proofs 仓库，采用 Apache-2.0 许可。我们检查了文件：十份全部能用 Lean 4.32 和 mathlib 编译，且没有一份含有'sorry'占位符或自定义公理这两个常见的逃生舱。
这十项，按 OpenAI 的表述：高维球体堆积的新上界，降至 Cohn-Elkies 阈值；二进制码和球面码的指数级改进界；非 sofic 群的构造；证伪 Connes 刚性猜想的反例；永久式的下界，包括一个 n 的四次方除以 log n 阶的算术公式下界；量子博弈的指数级并行重复定理；最近向量问题多项式因子近似难度；Ehrhart 体积猜想的精确答案；多色三角形 Ramsey 数的超指数下界，这将解决 Erdos 第 183 题；以及紧致性和退化性猜想的反例，解决 Erdos 第 146 和 180 题。OpenAI 的框架是每个问题都至少停滞了十年。这个框架是他们的，按 Sol API 费率约 2,000 美元总算力的数字也是他们的。
以下是今天可以独立核验的部分，比没有多，比证明少。可核验：仓库存在，十份 Lean 文件在内，内容如上所述，两份配套 PDF（论文和模型的推理叙述）可以下载，仓库还附带独立内核检验的配置。尚不可核验：OpenAI 之外没有人报告重建了这些证明；没有人类数学家评审过；也没有专家确认形式化命题与非形式定理同义，而这一步正是形式化可能悄悄出错的地方。最强的未被批准信号：参考追踪站 erdosproblems.com 仍把第 183 题列为开放，悬赏 250 美元，而一个较小的追踪站已在 8 月 1 日将其标为已解。该站维护者 Thomas Bloom 称这是'大新闻'，'就构造而言，这是大的'，这些话由 The Decoder 转引；我们未能直接取到原文。
在命名上必须精确，因为这篇将是人们回引的出处。博客写的是'Astra 的一个内部版本，我们的下一代主力模型'。'下一代主力模型家族'的说法来自 OpenAI 研究员 Noam Brown，他还补充说'遗憾的是没有千禧年难题（暂时）'，并指出该模型在其他重大问题上失败了。其余一切都是报道而非确认：The Information 经 The Decoder 转述，称 Astra 是与 Sol、Terra、Luna 并列的新模型类，GPT-6 还是 GPT-5.7 尚未决定，也没有发布日期。OpenAI 自己的伦理说明值得整段引用：'为一个完全由 AI 系统生成的证明声称人类作者身份，会同时歪曲系统的贡献和真正人类智力工作的性质'，公司表示他们为正确性负责，而论证本身由模型生成。等重建结果到来时，就该用这句话来要求他们。