先看证据
发布的不是模型，而是一批待审查的数学结果
2026年10月6日，OpenAI发布了一批由内部前沿模型生成的数学结果，并将论文稿、支持材料和部分 Lean 形式化证明放进 GitHub 仓库。发布面向的是开放研究问题上的数学进展，而不是一次模型上线：模型本身没有公开，外界拿到的是经过整理的结果及其部分证明材料。
这一区别决定了该如何读这批成果。OpenAI称，原有数学评测表现趋于饱和后，团队转向开放问题，并将模型输出整理成结果家族和稿件，再筛选达到一定重要性标准的内容；但公开资料没有定义这个标准，也没有交代每项结果如何被选中。因此，这不是一组可直接当作模型能力排名的分数，而是一批需要逐项理解、核验和评估的研究主张。
数字说明了规模，也说明不了成功率
仓库的规模数据值得先拆开看：目录收录722份稿件，归为372个结果家族；评测期间模型被提出约4,000道问题。稿件和结果家族不是同一计数单位，一个家族可能包含主要结果、相关论证、推论或替代证明，而4,000道是尝试题目数，不是已解决题目数。把它们混成一个“成功率”，会让读者误读这次发布实际展示了什么。
OpenAI还给出平均每项结果约相当于三小时 ChatGPT Pro thinking 的计算量，并公开了10项结果的推理摘要。前者是计算量估算，不是每项结果精确的运行时长或成本；后者也不是完整推理记录。它们让读者对投入和部分过程有了参照，却不足以独立重建实验，更不能单凭这些数字判断结果的质量或新颖性。
Lean能检查证明，不能替共同体做判断
Lean 形式化给这批研究增加了一层计算机可检查的证据。把证明写成 Lean 可识别的形式后，证明助手能够检查形式化论证是否成立，这比只公开一份自然语言证明多了一种明确的核验路径。OpenAI说仓库里有许多稿件包含形式化证明，也计划继续补充，但没有公布形式化总数，且并非每篇稿件都已形式化。
即使证明通过了 Lean 检查，数学工作中另外几类问题仍然存在：形式化是否准确对应论文中的主张，结果是否新颖、重要，以及证明是否依赖了恰当的定义和前提。对尚未形式化的稿件，OpenAI也提醒它们可能存在问题；公开材料没有给出所有稿件的独立核验结论。Lean能帮助检查特定形式系统内的证明，不会自动完成同行评审，也不会替数学家判断哪些结果值得纳入知识体系。
透明度增加了，但实验室仍在黑箱里
OpenAI没有只发布结论：仓库还提供论文修订和引用规范、部分推理摘要、计算量估算及尝试题量。这些做法为外部讨论提供了共同对象，也回应了数学界对理解、核验和吸收 AI 结果所需时间的关切。OpenAI称，发布前曾向数学与人工智能顾问组征求建议，但该组明确表示，参与建议不代表认可结果或为发布方式背书。
然而，外界仍无法从这些材料完整复现研究过程。具体模型名称、提示词和完整实验流程没有公开，模型筛选结果的标准也未说明；推理摘要只是摘要，而不是逐步记录。顾问组曾建议尽可能形式化每项结果，并披露模型、提示词、耗时和计算成本。比较这份建议与本次披露，可以看到改进方向，也能看到仍未填上的信息缺口。
把它当作研究入口，而不是研究结论
技术负责人和研究团队可以从中得到一个实际判断：AI 研究成果的发布质量，不只取决于模型是否给出正确答案，还取决于外界能否定位主张、检查证明、追踪修订并理解结果的来源。这次仓库提供了部分基础设施，尤其是 Lean 文件和引用、修订协议；但模型不可用、流程不完整，意味着外部团队不能把仓库等同于一次可复现的研究交付。
更稳妥的使用方式，是把论文视为待核验的研究线索，优先检查已有形式化材料，再由领域研究者判断主张的新颖性、重要性和适用范围。OpenAI提到的黎曼 ζ 函数零点自由区域工作也提醒读者，批次内部并非完全同质：相关稿件中，Re(s)>11/12 的一份稿件经过人工编辑以改善可读性，另有工作被说明为例外流程。可执行的判断不是“AI已经自主证明重要定理”，而是逐项问清证明是否可检查、研究过程披露到什么程度，以及哪些结论仍需独立审查。