OpenAI Astra模型攻克十年未解数学难题，单题成本不到2000美元

一句话看懂

OpenAI用内部模型Astra解决了十个十年未获突破的数学难题，单题成本不到2000美元，并公开了Lean 4形式化证明。

详细发生了什么

继Anthropic用Claude发现密码学弱点后，OpenAI也秀了一把肌肉。他们让”内部版Astra（下一代主要模型）“去解决十个数学问题，这些问题”主结果至少十年没有进展”。OpenAI声称，按GPT-5.6 Sol的token价格计算，每个问题的花费不到2000美元。（至于有多少问题花了2000美元却没解出来，OpenAI没提。）

OpenAI在GitHub上开源了openai/ten-proofs仓库，包含Lean 4形式化证明，还发布了一篇论文描述解法，以及一份LLM生成的PDF，模型根据未公开的推理轨迹”重建了证明的来龙去脉”。这种透明度值得肯定，但作者Simon Willison表示：“我更想看他们用的prompt！”

数学界对此反应强烈，很多人联想到1997年IBM深蓝击败卡斯帕罗夫的历史时刻。OpenAI的结果让Willison想起陶哲轩在IEEE Spectrum（6月刊）提出的”大数学”概念：陶哲轩既不轻视AI也不恐惧，而是视其为学科根本性转变的催化剂。

中文圈视角

对中文圈用户来说，这件事有几个值得关注的层面。

首先，数学研究离普通用户较远，但AI在形式化证明上的突破，可能间接影响编程工具。Lean 4是微软开发的形式化证明语言，国内开发者若想复现或学习这些证明，GitHub仓库是开放的，不需要梯子，但需要一定的数学和编程基础。

其次，国内大模型如DeepSeek、Kimi在数学推理上也有布局，但公开的”解决十年难题”案例较少。OpenAI这次展示的是模型在长链条推理和自主探索上的能力，这对国产模型是个提醒：推理能力不只是刷榜，更要能解决真实世界的难题。

最后，从合规角度看，这些证明和论文是公开的，不涉及数据出境问题，国内研究者可以直接使用。但要注意，OpenAI的模型本身在国内不可用，想复现实验需要自行解决访问问题。

几条值得记住的细节

OpenAI内部模型Astra解决了十个十年未获进展的数学问题，单题成本低于2000美元（按GPT-5.6 Sol token价格计算）。
开源仓库openai/ten-proofs包含Lean 4形式化证明，另有论文和LLM生成的推理重建PDF。
Anthropic此前用Claude发现密码学弱点，花费10万美元token，prompt明确要求”不要找低垂的果实”。
陶哲轩在IEEE Spectrum提出”大数学”概念，认为AI将推动数学研究范式转变。
作者Simon Willison呼吁OpenAI公开prompt，认为这是透明度的关键一环。

一句话总结

AI在数学证明上的突破，意味着推理能力正从聊天走向科研，中文圈可关注开源证明和国产模型差距。