OpenAI公开722篇AI数学手稿：最大规模公开基准背后的透明度博弈

2026年10月6日，OpenAI在GitHub上线名为openai/math的公开仓库，采用Apache-2.0协议发布722篇数学手稿，归入372个问题族，附带Lean形式化证明文件和模型推理摘要。产出这批成果的是一款未公开的内部前沿模型，据unite.ai报道，其能力显著强于GPT-6 Astra。这是迄今为止规模最大的AI数学输出公开集。

这批手稿的生产方式相对固定：模型被输入约4000道开放数学问题，通过显著性筛选和成果归组，最终形成722篇手稿。OpenAI披露，平均每项入选结果消耗的算力相当于约三小时ChatGPT Pro思考。

四类核心成果，含金量参差

从网易科技等中文媒体的技术梳理来看，这批手稿中最受数学界关注的有四类：

• 准黎曼猜想（Quasi-Riemann）：手稿声称证明了黎曼ζ函数在实部大于7/8的区域内没有零点。罗格斯大学数学教授Alex Kontorovich在看到这一结果后公开表示：“如果是人类做出来的，立刻就是一枚菲尔兹奖，毫无疑问。”完整的黎曼猜想并未因此宣告解决，但这一固定宽度零点禁区的拓展，被认为在技术上远超此前预期。该结果附有Lean形式化材料。
• 霍奇猜想特殊情形：针对CM阿贝尔簇上有理霍奇猜想给出证明。霍奇猜想是七大千禧年难题之一，此次处理的是其中一个特殊但重要的类别，尚未给出完整的Lean形式化。
• 唯一博弈猜想（Unique Games Conjecture）：手稿声称给出证明，并由此推导出Max-Cut等问题的近似难度界限。在P≠NP的前提下，这意味着某些计算问题高效算法的近似保证无法突破相应理论下界。
• 自由群因子问题：论文给出结论，覆盖所有参数大于1的插值自由群因子，包括无穷参数情形，并附有Lean形式化材料。

仓库README还披露了两个例外情形：黎曼ζ函数相关手稿和霍奇猜想手稿是仅有的两篇偏离固定流程的成果，其中黎曼ζ函数的写作经过人工编辑以提升可读性。

Lean形式化：验证基准，但覆盖有限

此次发布中，Lean形式化证明是技术可信度的核心依托。Lean是一种允许数学证明被计算机逐步核查的编程语言——它不接受“显然成立”的跳跃，每一步推导都必须通过逻辑规则验证。

据公开目录统计，722篇手稿中约162篇主结论附有Lean形式化材料，其余均未完成计算机验证。OpenAI在README中明确承认，部分未形式化结果可能存在问题，并承诺持续修订。仓库仅包含10份模型推理过程的摘要，而非全量推理链路，这意味着研究人员无法系统性地追溯每个结论的生成逻辑。

康奈尔大学数学副教授Daniel Halpern-Leistner正在开发自动形式化工具，他此前对媒体表示：“现在这件事显得非常紧迫，因为用自然语言写出的论证正大量涌来。”他同时指出了一个关键边界：机器检查的是代码中定义的命题，若代码定义本身与原始数学问题之间存在偏差，形式化通过也无法为整篇论文背书。准黎曼成果的Lean说明就明确注明，论文的后续应用部分不在该形式化的覆盖范围之内。

这不是对Lean形式化的否定，而是对其边界的精确描述：它是迄今最严格的AI数学输出验证机制，但“主结论有Lean”与“全文所有结论均可信”之间仍有实质性距离。

AGMAI：被迫介入的学术治理

这次发布背后，还有一个此前较少被关注的治理机制——AGMAI（数学与人工智能咨询组），由普林斯顿高等研究院（IAS）主持，成员涵盖菲尔兹奖得主Timothy Gowers、Martin Hairer和Edward Witten等顶级数学家。

AGMAI的诞生本身就带有被动性。今年9月初，OpenAI就Navier-Stokes相关结果的发布方式受到学术界批评，此后才与IAS合作组建了这个咨询机制。AGMAI在9月29日正式发布负责任发布建议，这份建议来自对数学界600余份回复的系统梳理，其核心内容包括：AI机构发布数学成果时，应披露模型名称、提示词、推理摘要和计算成本，并将论文存档于“不在任何AI公司控制下的学术库”。

AGMAI还特别点名警告：不得将数学成果发布当作宣传模型的营销工具，称这种做法“已对数学界造成重大伤害”。

这一告诫并非空穴来风。据媒体报道，今年8月，OpenAI曾召集约40位数学家参与闭门会议，暗示模型已解决数百道难题，会上有参与者认为公司承诺不会一次性集中发布；但OpenAI发言人事后表示，不知道有过这个保证。双方对于是否存在承诺本身都没有共识。

此次10月6日的发布，无论在规模上还是透明度标准上，都与8月那次争议形成了鲜明对比。OpenAI在仓库中设置了版本管理机制，记录所有修订历史，保留旧版本可访问，并为每篇手稿提供BibTeX引用格式——这是学术规范的标配，但在AI公司主导的研究发布中并不常见。

标准评测饱和之后

OpenAI在README中解释了这批手稿的评测背景：模型在既有数学评测集上的表现已接近饱和，迫使评测团队将更多开放数学研究问题纳入考卷。这是一个在AI能力追踪领域具有结构性意义的信号——当标准化基准不再能区分顶尖模型，如何设计可信的前沿评测，本身成了一个需要解决的方法论问题。

此次发布的722篇手稿，实质上为这个问题提供了一类新的参照系：可复现、可引用、部分可形式化验证的真实开放数学问题集。372个问题族按数学分支分类，每个家族内部包含主结论、配套论证、推论和替代证明，允许研究者从不同角度切入验证。这与以往AI数学能力的展示方式——主要通过竞赛题集或封闭评测——存在质的差异。

西北大学数学家Bryna Kra在发布前接受WIRED采访时说：“这是个令人不安的时刻，但也着实令人兴奋。”

独立判断

这次发布的意义，不只是数学成果本身的含金量，而在于它建立了一个先例：AI机构可以在学术咨询框架下，以可引用、可版本追溯、可形式化验证的方式公开前沿模型的推理输出。这套机制若能被其他AI机构复制，将为AI输出的学术可信度建立一条结构性通道。

这次发布存在两处待观察点。其一，Lean形式化的覆盖缺口是实质性的，722篇中约560篇尚未完成计算机验证，而未形式化结果是否存在系统性问题，目前无法排除。其二，AGMAI建议存档于“独立学术库”的诉求尚未完全落实——OpenAI选择的是自己控制的GitHub仓库，这在技术层面符合开放性要求，但在机构独立性上仍与AGMAI的理想标准存在距离。

可复现、可验证的AI数学输出从今天起有了一个规模最大的公开基准。这是真实的技术进步。接下来的问题，是数学界能以多快的速度完成对372个问题族的独立评估——这个速度，将决定这批手稿是否最终被学术共同体接纳为有效知识。