OpenAI 称 AI 攻克十个长期停滞的数学问题

OpenAI 最近展示了一组面向数学与理论计算机科学的 AI 研究成果：他们让一个名为 Astra 的内部版本模型尝试解决十个数学问题。这些问题据称在核心结果上至少十年没有取得进展。

主要信息

OpenAI 表示，这些问题中的每一个，在按 GPT-5.6 Sol 的 token 价格估算时，成本都低于 2000 美元。

不过，有一个关键细节并未披露：他们一共尝试了多少个问题，以及有多少问题同样花费了类似成本但没有得到解法。因此，目前只能看到成功案例，无法判断整体成功率。

形式化与透明度

OpenAI 提供了这些结果的 Lean 4 形式化版本，并发布了一篇解释解法的论文。此外，还有一份由大模型生成的说明文档，用于根据未公开的推理轨迹重构证明形成过程。

这比单纯发布结论更透明，因为形式化证明至少为外部验证提供了基础。但仍有一个重要缺口：实际使用的提示词没有公开。对于评估模型能力、复现实验过程以及理解人类研究者在其中的作用来说，提示词非常关键。

与近期 AI 科研展示的对比

就在几天前，Anthropic 也展示了 Claude 在密码学弱点发现方面的能力。据称该实验使用 Mythos Preview，花费约 10 万美元 token 成本，并在提示中明确要求模型不要寻找“低垂的果实”，而是进行真正困难的研究探索。

相比之下，OpenAI 这次强调的是数学问题求解，并声称单个成功案例的计算成本低得多。但两者共同指向一个趋势：大模型正在被用于更接近前沿研究的问题，而不只是完成编程、写作或问答任务。

“大数学”的可能方向

这类结果让人联想到陶哲轩曾提到的“big mathematics”概念：未来的数学研究可能会转向更大规模的人机协作。复杂任务被拆分成许多子任务，人类负责创造性判断、问题设定和方向选择，AI 则承担大量技术性推导、验证和搜索工作。

这并不意味着 AI 已经可以独立取代数学家。更合理的理解是：如果这些结果经得起审查，AI 可能正在成为数学研究中的新型基础设施，尤其适合处理形式化、搜索密集、细节繁重的部分。

仍需关注的问题

目前最值得继续追问的不是“AI 是否解决了十个问题”这么简单，而是：

• 这些问题的选择标准是什么？
• 失败案例有多少？
• 人类研究者在过程中承担了多少筛选、引导和修正工作？
• 未公开的提示词是否会显著影响可复现性？
• Lean 4 形式化结果能否被独立审查并确认无误？

在这些问题得到更多解释之前，这项进展可以被视为一次重要信号：AI 正在进入数学与理论计算机科学更核心的研究流程。但它究竟代表工具效率提升，还是研究范式转折，还需要更多可复现、可审查的案例来判断。