OpenAI于2026年公开了一批由内部未发布前沿模型生成的数学研究材料，在GitHub上发布722份手稿与相应的版本与证明记录，并提供部分Lean形式化代码以便外部检验。公司强调这些成果处于不同核验阶段，尚未得到数学界全面独立确认，并披露了模型尝试数量与计算开销等透明化信息。
OpenAI于2026年10月6日发布文章《Sharing AI progress in mathematics》，公开一批由内部未发布前沿模型生成的数学研究成果，并同步上线GitHub仓库。仓库目前收录722份手稿，按相关性整理为372个成果系列；其中许多结果配有Lean形式化材料，供计算机检查证明中的逻辑步骤。
这次发布的重点不只是“AI解决了多少数学问题”，也在于OpenAI试图把模型生成的研究过程、计算开销、版本修订和形式化验证一起置于公开环境中。不过，公司同时强调，这些材料处于不同的核验阶段，尚未获得数学界对全部结果的独立确认。
从模型输出到可供复核的研究材料
OpenAI在官方公告中说，研究结果来自一个尚未公开的内部模型。公司将相关手稿、证明辅助材料、引用和论文修订协议放入OpenAI数学成果GitHub仓库，并表示会保留公开发布历史，让后续修订和更正能够追溯。
仓库说明称，成果覆盖数学的多个分支，并包括纯数学、理论计算机科学和数学物理等方向。一个“成果系列”可能包含主要结果、伴随论证、推论或替代证明，因此722份手稿并不等同于722个彼此独立的数学发现。
OpenAI还公开了10份模型推理过程的摘要，以及尝试题目数量和计算开销的估计。按照仓库和公告中的说法，模型在评估过程中大约被提出了4,000个问题；平均每项结果消耗的计算量，相当于ChatGPT Pro约3小时的思考用量。这里的“结果”是OpenAI对研究产出的统计口径，不应直接理解为每个结果都已成为数学界认可的定理。
Lean形式化提高可检查性，但不等于同行评议
Lean是一种用于形式化数学证明的编程语言。研究人员可以把定理、定义和推导步骤写成形式化代码，再由证明助手检查代码是否符合指定逻辑系统的规则。
这类检查为AI生成的数学成果增加了一个重要的技术层：外部研究者可以下载代码，检查它是否能够在相应环境中构建，以及证明步骤是否通过Lean内核的验证。OpenAI表示，仓库已包含许多证明的Lean形式化版本，并将在完成更多工作后继续补充。
但形式化验证的边界同样重要。Lean可以检查代码中的逻辑链条，却不能单独判断一个数学命题是否重要、定义是否准确表达了论文想讨论的对象，也不能替代人类研究者对既有文献、论证语义和研究贡献的判断。OpenAI的仓库明确提醒，部分尚未形式化的结果可能存在问题，公司将努力尽快修正。
这一区分在近期的AI数学项目中已经反复出现。比如，AIFlux此前报道的OpenAI内部AI系统生成并形式化验证纳维–斯托克斯方程解也指出，机器可检查的形式化材料并不能替代外部数学家对问题定义、边界条件和证明含义的独立审查。
OpenAI试图回应数学界的透明度要求
这次发布的方式，与OpenAI近期成立数学与人工智能独立顾问组的安排相互衔接。该顾问组由普林斯顿高等研究院托管，成员包括多位数学家，职责涉及AI生成数学成果的审查、发布方式、归属和研究生态影响，但并不负责决定OpenAI内部研究的速度，也不是逐项证明的认证机构。相关背景可参见OpenAI成立数学与人工智能独立顾问组的报道。
OpenAI表示，它在准备这次发布时参考了该顾问组以及数学界公开提出的建议。公司承诺继续改善论文中的引用、数学表述和展示方式，并探索符合数学界建议的社区托管方案。公司还计划资助围绕AI生成重大数学成果的研讨会、会议和特别项目。
这意味着OpenAI披露的对象不再只是最终论文，而是包括模型产生结果的过程、尝试规模、计算成本估计、证明代码和版本历史。对研究者而言，这些信息有助于判断结果的来源和可复现程度；对公司而言，这也把“模型声称取得突破”转化为一个需要长期维护和接受外部检验的公开研究档案。
“公开结果”距离“数学界接受”仍有距离
OpenAI没有把这次材料描述为已经获得学术界接受的完整成果，也没有声称所有公开手稿都解决了公认的开放难题。现阶段能够确认的是：公司公开了一批由内部模型生成的数学研究材料，并提供了部分Lean形式化证明、推理摘要和计算统计。
尚不能据此确认的事项包括：每一项结果是否正确、哪些结果具有足够的数学重要性、形式化代码是否覆盖了论文中的全部关键主张，以及这些成果能否经受独立研究者的重复检查。对于尚未形式化的手稿，外部复核还需要依赖传统的论文阅读、推导检查和同行讨论。
AI参与数学研究的争论，因此并不只围绕模型能否生成答案。更核心的问题是，研究成果应如何被解释、引用和归属，数学共同体能否在不依赖公司声誉的情况下复核结果，以及计算资源和封闭模型是否会让少数公司掌握越来越多的研究议程。
OpenAI的这次发布为这些问题提供了一个更具体的观察对象：722份手稿、372个成果系列和部分机器可检查证明，构成了一个规模较大的公开实验。但在独立数学家完成审查之前，最稳妥的结论仍是，OpenAI公开了值得研究的模型生成数学成果和验证材料，而不是宣布数学界已经确认了一批新的定理。
来源：