OpenAI在8月1日发布了一份题为《Ten advances in mathematics and theoretical computer science》的报告,称内部模型Astra一口气攻克了十道数学与理论计算机科学难题,涵盖球体填充、Connes刚性猜想证伪、多色Ramsey数(Erdős问题183)等一批数学家真正在意的问题。配套材料相当扎实:一份253页的技术手稿,一份62页的"数学发现笔记",外加用Lean 4.32.0编写的形式化证明,全部开源在GitHub仓库里。这套阵仗确实吓到了不少人,但眼下最该被追问的,不是"AI又解出了什么",而是这十个证明到底有谁核实过。
答案是:目前基本没有独立数学界的完整复核。这才是这场"数学存在性危机"最容易被忽略的地基问题。
一份自证清单,配了极其专业的包装
OpenAI这次没有像以往那样只放一篇通稿,而是把手稿、推理笔记、Lean证书、GitHub仓库全部打包给外界审阅——这种透明度在AI公司里少见,值得肯定。但透明不等于验证。253页手稿讲的是模型怎么想到解法,62页笔记重构的是它哪些初始思路走通了、哪些走不通,这些都是"过程说明",不是第三方审核结论。
真正承担验证角色的是Lean证书:把数学证明翻译成代码,跑一遍能通过,就说明逻辑链条自洽。但OpenAI自己的官方页面写得很清楚——Lean证书成立的前提是,形式化陈述必须准确对应原始的非形式化数学声称,假设条件和公理导入也要恰当。换句话说,机器验证的是"如果这样表述,逻辑对不对",而不是"这样表述本身有没有偷换概念"。这道核查关卡,目前只能靠人,而《The Verge》采访的数学家提到,愿意逐字读完全部材料的人,全世界大概只有几十个。
同一枚"金牌",含金量不一样
想判断这场危机有多实,得把它放进2024年到2026年的完整赛道里看。2024年,DeepMind的AlphaProof加AlphaGeometry2在IMO拿到28/42,银牌水平,但要靠人工先把题目翻译成形式化语言,耗时数天。2025年跳到端到端自然语言推理:DeepMind的Gemini Deep Think和OpenAI同期的内部模型都报出35/42,金牌线以上。
区别在于认证方式。DeepMind这35分是经IMO官方认证评分的,OpenAI那35分是自评自报,没有走同等的第三方认证流程。今年7月上海IMO的官方金牌线是29/42,666名人类选手里只有7人满分——这个基准线摆在那,再看两家公司同样标出"35/42",可信等级完全不同。
分数一样,认证不一样,危机感却一样重
2026年5月,OpenAI宣布模型证伪了一个关于平面单位距离的Erdős猜想,这次是经外部数学家核实的,算是一次干净的独立验证案例。而8月这十项结果,目前还停留在OpenAI单方面公告加自建证书的阶段。同期,DeepMind走的是另一条路:2月推出研究型智能体Aletheia,采用生成—验证—修正的架构,在IMO-ProofBench Advanced测试里靠堆推理算力做到约九成正确率,主打的是可持续、可规模化的证明流水线,而不是一次性甩出一批重磊成果。两家公司对"数学AI应该证明什么"的理解,分岔得越来越明显。
谁在焦虑,谁在讲故事
数学家们的存在性危机是真实的,也合乎逻辑:如果AI能在专业水准上解决前沿难题,那学术资助该怎么分配、博士该培养来做什么、职业价值又建立在哪里,这些问题确实无解。但把这种危机感和"AI已经攻克数学"这个尚未坐实的判断绑在一起,风险不小。
- 提醒.十项结果目前只完成了自我证书,独立同行复核还没跑完,危机叙事跑在了验证前面。
对一线研究数学家来说,现实的动作不是恐慌离场,而是多一项新工作——审查AI生成的证明,这本身就要占用本该做原创研究的时间。对高校和资助机构来说,眼下更该做的不是急着改资助逻辑,而是先建立一套应对AI证明的审查规范。对AI实验室而言,数学突破本来就是重要的公关筹码,一份写得比学术论文还漂亮的技术报告,本身就是营销物料的一部分,这不代表内容有假,但也不该被当成已经盖章的事实。接下来真正该盯的,是这十个证明能不能等来一次干净的独立复核,以及OpenAI是否愿意像DeepMind一样,把下一次成果拿去接受第三方认证。