OpenAI 用 Astra 模型解决十个数学难题

2026 年 8 月 1 日，Simon Willison 的博客报道，OpenAI 宣称其“下一个主要模型的内部版本 Astra”解决了十个数学问题，这些问题“主要结果至少十年没有进展”。据称，每个问题的 token 成本低于 2000 美元（按 GPT-5.6 Sol 价格计算）。

OpenAI 在 openai/ten-proofs 仓库中提供了 Lean 4 形式化证明，并发布了一篇描述解决方案的论文，以及一个 LLM 生成的 PDF，其中模型基于未公开的推理轨迹“重建了证明的诞生过程”。

Willison 评论称这是“相当程度的透明度”，但他表示“我想看到他们使用的提示词！”。

OpenAI 声称每个问题的成本低于 2000 美元，但 Willison 指出：“没有关于他们花了 2000 美元却未解决问题数量的消息。”这暗示成功率可能并非 100%，但未公开具体失败案例。

相比之下，Anthropic 几天前使用 Claude 和 Mythos Preview 发现密码学弱点，花费了 10 万美元的 token 费用，提示词中强调“我们不是在寻找低垂的果实，我们想要真正的研究来发现真正困难的发现”。

OpenAI 的透明度体现在公开形式化证明和论文，但提示词的缺失使得可复现性受限。Willison 的评论表明，提示词是评估研究质量的关键。

Willison 观察到“许多数学家在线经历了一场集体的‘深蓝时刻’”，暗示 AI 在数学上的突破类似于深蓝击败国际象棋冠军的历史性时刻。

他引用了陶哲轩在 6 月 IEEE Spectrum 中的观点：陶哲轩既不轻视 AI 也不恐惧，而是将其视为学科根本性转变的催化剂，即“大数学”——大规模、去中心化的人机协作，人类负责创造性部分，AI 承担大部分技术性工作。

这一背景为 OpenAI 的结果提供了框架：AI 并非取代数学家，而是作为工具扩展人类能力。

确认的事实：OpenAI 发布了 Lean 4 形式化证明、论文和 LLM 生成的 PDF；Anthropic 花费 10 万美元 token 费用发现密码学弱点；陶哲轩在 IEEE Spectrum 中提出“大数学”概念。

来源声明：OpenAI 声称解决了十个问题，每个成本低于 2000 美元；这些声明来自 OpenAI 的公告，但未经独立验证。

不确定性：未披露失败案例数量；提示词未公开；成本计算基于 GPT-5.6 Sol 价格，但实际 token 使用量未知；数学问题的难度和重要性未详细说明。