OpenAI称内部模型解出十道十年数学难题：证明公开，失败率没公开

OpenAI公布了一份战报。内部代号Astra的模型解出了10个数学与理论计算机科学难题,这些问题至少十年没有实质进展。官方给出具体成本:按下一代模型GPT-5.6 Sol的token价格算,每道题不到2000美元。

公开材料包括一篇论文、openai/ten-proofs仓库里的Lean 4形式化证明代码,还有一份模型自己生成的"推理复盘"PDF。

这套材料能证明的,是证明本身经得起Lean的机器检验。证明不了的,是这十个解法背后有多少次失败尝试、用了什么提示词、模型真实的推理轨迹长什么样——OpenAI一个都没公布。把这次结果读成AI已经能独立完成原创数学研究,证据目前还不够。

发生了什么：十个难题,一个没公布的分母

十个问题具体是什么,论文和仓库里都列了出来。共同点是:主流数学界至少十年没能推进这些结果的证明。OpenAI这次没有挑简单题,这本身是个可核查的事实锚点。

Lean 4形式化意味着什么？证明检查器会逐步验证每一条逻辑是否成立,这是数学界公认的硬门槛,比自然语言证明更难蒙混过关。这部分可信,同行现在就能去仓库里跑一遍检查器核实。

证明能被形式化检查,不等于研究过程能被检查

但那份"推理复盘"PDF是另一回事。它是模型基于未公开的原始推理过程,事后写出来的叙事文本,读起来像模型在讲它当时怎么想。真实的推理轨迹从没公开过,这更接近事后包装,不是思考记录。

为什么重要：2000美元和10万美元算的不是一回事

几天前Anthropic公布了另一份材料:用Claude(Mythos Preview)去发现密码学弱点,一次调查花了约10万美元的token成本。提示词写得很直白——"不要捡低垂的果子,要真正难的发现"。

两份材料统计的不是同一件事。拿2000美元跟10万美元比,得出"OpenAI更便宜"的结论,是拿两把不同的尺子量东西。

更关键的缺口在分母上。OpenAI没说一共尝试了多少道题、在没解出来的题目上花了多少钱。公开的低成本只是十个胜出案例的数字,不是整套研究流程的真实开销——这个分母现在等于未知数。

数学与理论计算机科学研究者现在能做的,是把Lean验证通过的证明当作可核查候选结果,自己跑一遍仓库里的检查器,而不是直接采信论文叙述的证明过程。

评估AI科研工具预算的技术负责人,更该做的是问清楚供应商的成功率和总成本,而不是只看胜出案例的单价——2000美元这个数字暂时套不进ROI模型。

接下来看什么：证明过了机器的关,研究过程还没过关

今年6月陶哲轩在IEEE Spectrum提过一个说法:AI正在催生"大数学"(big mathematics),人类和机器分工协作,人做创造性判断,AI做技术性苦力活。OpenAI这次的操作落在这个方向上——Lean形式化证明这类可验证的技术性工作,确实是当下AI能稳定交出价值的地方。

接下来值得盯的,是三件还没发生的事:有没有独立数学家复现或审查这十个证明、OpenAI会不会补上失败率和总尝试次数、提示词会不会公开。三件事只要有一件兑现,这次结果的可信度都会往上走一格。