OpenAI在2026年10月6日正式公开名为openai/math的代码仓库，公布了内部前沿模型在高级数学领域的最新产出。发布内容包括722篇手稿、372个成果家族，涵盖Mahler猜想、Kaplansky型猜想、Vlasov–Maxwell系统、Crouzeix不等式、Ramsey构型以及矩阵乘法界限等多个经典数学难题。然而，就在公开发布的同一天，普林斯顿高等研究院数学与人工智能咨询小组（AGMAI）明确发出声明，向OpenAI提供规范建议并不构成对其成果或获取过程的背书。
热闹的公关叙事之下，藏着严谨科研与工程宣发之间的巨大断层。
算力堆叠出的手稿账本
根据披露的数据，这批成果总共消耗了约12,000小时ChatGPT Pro的思考等效算力，平均每个报告出的成果耗时约3小时。整个实验测试了约4,000个数学问题，最终筛选并打包出722篇论文手稿。
这个消耗水平表明，团队并非让模型展现一蹴而就的顿悟，而是依托自动化流程执行了大规模的启发式搜索。数学探索往往包含极高比例的试错，但将海量尝试直接封装为数百篇学术手稿推向公共视野，在数学界实属罕见。
历史上每一次计算工具进入纯数学领域，都会引发关于证明本质的讨论。1976年阿佩尔与哈肯借助计算机验证四色定理时，学术界尚且耗费数年核验代码逻辑。古人云：工欲善其事，必先利其器。工具的革新从来值得鼓励，但工具吐出的海量印刷品并不能直接等同于已被确立的知识。
- 结论.平均3小时的思考算力更接近针对特定解题路径的并行暴力搜索，而非科研范式的根本颠覆。
形式化验证里的未验折扣
宣发中最引人注目的标签是Lean形式化验证。Lean是一种允许计算机严格核对证明步骤的语言，被视为消除大模型幻觉的终极过滤器。但在722篇手稿中，仅有162篇在Lean中形式化了主要结论。
更为关键的是细节披露：在这162篇形式化文件中，目录状态被明确标注为部分进展，形式化审查状态则全数标为未检查（unchecked）。这意味着不仅超过七成的手稿完全没有经过形式化逻辑核验，剩下的两成多代码也仅仅是完成了代码层面的编写，尚未经过严密的交叉审读。
代码编译成功，与数学论证成立之间，隔着整整一个现代数学共同体。
OpenAI在附带说明中也做出了保留，承认未形式化的结果可能存在缺陷。没有严密形式化保障的自然语言长篇论证，面对复杂的现代前沿猜想，极易在隐蔽的引理推演中滑入逻辑漏洞。
避重就轻的学术规范博弈
AGMAI在2026年9月29日发布的指导规范中，明确呼吁AI实验室停止在无法访问的专有闭源模型上测试前沿高级数学问题，并警惕将数学论文当成商业营销手段。同时，规范主张论文应托管于独立的学术预印本库，而非企业自身控制的平台。
对比之下，OpenAI的动作显得颇有妥协意味。所有产出依然放置在自家的GitHub仓库内；4,000次攻题尝试中，仅披露了10份节选推理摘要；生成成果所依赖的核心底层模型，依旧未对学术界公开。
纯数学领域的研究者正面临双重挤压：一方面他们缺乏同等规模的算力资源去重现这些推导，另一方面却要承受筛查和修补数百篇AI生成预印本的无偿劳动力负担。当企业将未筛查的手稿倾倒进学术网络，实质上是将质检成本单向转移给了外部科研共同体。
- 提醒.缺乏可复现环境的批量科研成果，会大幅推高学术界的审阅鉴别成本。
竞赛刷分与科研探索的落差
在数学评估体系里，解题与做研究是两套截然不同的逻辑。
Google DeepMind此前推出的AlphaProof与AlphaGeometry 2系统，依托强化学习与Lean搜索，在IMO 2024取得了28/42分，达到银牌等效水平。其中AlphaProof解出了5道非几何题中的3道，AlphaGeometry 2攻克了那道几何题。
竞赛题目边界清晰、目标明确，适合符号搜索和强化学习定向突破。然而在Epoch AI设立的科研级基准FrontierMath上，主流通用大模型此前的早期得分仅处于低个位数。科研级数学需要学者自行定义新概念、识别虚假假设并在极长周期的逻辑荒原中寻找路径，这与预设好答案的刷榜完全不同。
722篇未充分核验的手稿，标志着生成式模型开始大规模介入符号推理的高地，但它并没有证明AI已经跨越了原创性科研的门槛。接下来整个领域的检验焦点，在于数学同行能否在openai/math中证实哪怕几个核心猜想的反例，以及技术提供方是否愿意真正开放模型，接受可复现性的阳光普照。