封面图来源：OpenAI 官网博客配图
北京时间 10 月 7 日早上 6 点 19 分，OpenAI 在 GitHub 上一次性公开了 722 篇数学论文，分成 372 组结果。全部出自一个还没发布的内部模型。
清单里有不少响当当的名字：准黎曼猜想、卡塔兰常数的无理性、矩阵乘法指数、霍奇猜想的一个特殊情形……
先说清楚：这些都是 OpenAI 自己报告的结果，大部分还没经过同行评审。仓库首页也写了，没形式化的那部分「可能有问题」。
GitHub 仓库
https://github.com/openai/math
OpenAI 官方博客
https://openai.com/index/sharing-ai-progress-in-mathematics/
OpenAI 官方账号的原话：
We're releasing a broad range of new mathematical results produced by an internal frontier model. We've been consulting with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, and we have drawn on their advice and public recommendations to inform how we release these results.
我们正在发布一大批新的数学结果，它们由一个内部前沿模型产出。我们一直在咨询高等研究院（IAS）的独立机构「数学与人工智能顾问组」，并参考了他们的建议和公开的推荐做法，来决定怎么发布这些结果。
@OpenAI 官方帖，北京时间 10 月 7 日 6:19（截图中空白的链接预览已裁去）
这事怎么来的
这不是 OpenAI 第一次在数学上放大招。
9 月初，OpenAI 宣称内部模型解决了纳维-斯托克斯方程这道千禧年大奖难题，在数学界吵得很凶。很多人不满的是：只宣布结果，不给细节，也不给人用模型。
9 月 21 日，OpenAI 又发了一篇公告，说这个 8 月 28 日开始训练的内部模型，已经解决了 100 多个长期悬而未决的问题。同时宣布，会听取一个独立数学顾问组的意见。
今天这批 722 篇，就是这些结果的正式公开。
IAS 和这个顾问组是谁
IAS 是美国普林斯顿的高等研究院，1930 年成立，爱因斯坦、哥德尔、冯·诺依曼都在这里待过，是全世界最顶尖的纯研究机构之一。
「数学与人工智能顾问组」（AGMAI）挂靠在 IAS，成员一共 9 位，个个是大牛：菲尔兹奖得主高尔斯（Timothy Gowers）、海雷尔（Martin Hairer）、威滕（Edward Witten），还有德莱利斯、瓦基尔、伍德、斯里瓦斯塔瓦、蒂尔曼、夏尔等人。
它的来历挺有意思。OpenAI 原本想找人组建一个外部顾问委员会，几位数学家商量后决定，干脆成立一个独立小组，再邀请其他人加入。
官网写得很直白：不拿任何 AI 公司的钱，建议全部公开，但没有决策权，最后怎么做由公司自己负责。
9 月 29 日，顾问组根据 600 多份数学界问卷，发布了一份「负责任发布 AI 数学成果」的建议。开头第一段就不客气：他们不认同 AI 公司拿内部专有模型去攻高难数学题，并且希望停止这种做法。
建议里的几条硬要求：
• 结果要放进不受 AI 公司控制的学术存档，有永久可引用的编号，修改有记录
• 每个结果都要公开模型名、提示词、思维链摘要、耗时和算力成本
• 能形式化的证明尽量形式化，要带 Comparator 题面文件和 formalization.yaml
• 批量发布时，要说明还试了多少同等难度的题没做出来，题是怎么选的
• 相关文献要查全、引用到位，别把发布成果当成给模型做营销
10 月 6 日，顾问组又专门发了一段声明：提供建议不等于认可这些结果的分量，也不等于认可 OpenAI 的做法。至于建议执行得怎么样，要由整个数学界来评判。他们说，公开只是开始：人类理解这些结果的过程才刚起步，远没有完成。
OpenAI 照做了多少
对照一下，有做到的，也有没做到的。
做到的：放出了 10 份模型推理过程的摘要；公布了每个结果平均花的算力，大约相当于 ChatGPT Pro 思考 3 小时；说明了总共给模型出了约 4000 道题，再按重要性筛出这 372 组。很多证明附上了 Lean 形式化，也确实带了 Comparator 题面和 formalization.yaml。
没做到的：模型名没公布，提示词没公布，算力只给了平均数，不是每题单列。存档目前放在 OpenAI 自己的 GitHub 上，博客说还在找社区托管的方案。
OpenAI 还说，会资助一批研讨会、会议和专项项目，帮助大家理解这些结果，细节以后再公布。
仓库里到底有什么
我们把仓库克隆下来翻了一遍。结构很清楚：
openai/math 仓库首页，只有一次提交，提交者显示为 Anonymous，许可证是 Apache-2.0
拆开来看：
• preprints：722 篇论文，每篇一个文件夹，有 PDF、LaTeX 源文件和一段 BibTeX 引用。引用信息里作者统一署名 OpenAI，日期大多在 9 月 23 日到 10 月 5 日之间
• overview.pdf 和 CONTENTS.md：总目录。372 组结果按 17 个方向分类，理论计算机最多，有 40 组；组合数学 37 组，代数与复几何 36 组，数论 31 组
• lean：Lean 形式化代码，12 万多个文件，超过 2500 万行
• reasoning_traces：10 份推理摘要，比如 π 的无理性指数、马勒猜想、自由群因子同构
结果的类型也挺杂：
• 证明了某个猜想，比如准黎曼猜想、哥德菲尔德猜想
• 给出反例，推翻某个猜想。光标题里写着「反例」的就有 34 组，比如卡普兰斯基直接有限性猜想在特征 2 下的反例
• 把某个界推到新纪录，比如矩阵乘法指数
• 把某个速率算到最精确，比如随机对称符号矩阵变成奇异矩阵的概率
几个细节值得一提。
README 说，绝大多数结果用的是同一套固定流程。例外有两个：黎曼 ζ 函数零点区域的一项工作，和 CM 阿贝尔簇上霍奇猜想的证明。其中 ζ 函数 11/12 那篇，还经过了人工润色。
署名方面，有一组随机 SAT 问题的结果，OpenAI 主动写明：阈值存在性这个猜想，是研究者 Gaia Carenini 在 10 月 5 日公开的论文里率先解决的，优先权归她，OpenAI 这边算另一种证明。
版本方面，OpenAI 承诺保留全部发布历史。勘误和修订都作为新版本记录，旧版本一直能看到。
Lean 验证是怎么回事
Lean 是一种能让电脑逐行检查证明的编程语言。证明写成 Lean 代码，只要编译通过，就说明每一步推理都站得住。
仓库的 372 组结果里，235 组附了 Lean 形式化说明。形式化目录里一共登记了 185 条主定理。
检查的办法叫 Comparator。每个结果有两个文件：一个是题面，只写定理该长什么样，证明部分空着，用 sorry 占位；另一个是完整证明。Comparator 负责核对：完整证明证的就是题面那句话，而且只用了 Lean 的 3 条标准公理。
这样一来，你不用看懂几十万行证明，只要看懂题面这几行，确认它说的就是那个数学问题。
比如下面这两个题面文件：
仓库 lean/ComparatorChallenges 下的两个题面文件，第一行注释是我们加的中文说明
要注意两点。第一，formalization.yaml 里写着形式化由智能体完成，审查状态是 unchecked，也就是还没人工审过。第二，OpenAI 也承认，形式化有时只覆盖论文的一部分结论。
我们没有在本地编译这套 Lean 库。官方说整个库非常大，建议一次只编一小部分。
挑两个结果说说
第一个：准黎曼猜想。
黎曼 ζ 函数和素数分布紧紧绑在一起。它的「非平凡零点」都落在一条宽度为 1 的带子里，也就是实部在 0 到 1 之间。
大名鼎鼎的黎曼猜想说：这些零点全都在正中间那条线上，实部恰好是 1/2。
这太难了，所以退一步，有个弱一点的版本，叫准黎曼猜想：能不能找到一个比 1 小的数，保证实部比它大的地方一个零点都没有？
在这之前，数学家只知道实部等于 1 的那条边上没有零点，而且越往高处，离边能保证的无零点区域就越窄。
OpenAI 的论文说，这个数可以取 7/8。也就是实部大于 7/8 的地方，ζ 函数没有零点，所有狄利克雷 L 函数也一样。另一篇论文用不同方法证明了 11/12。
要是成立，这会是解析数论里非常大的进展。但它不是黎曼猜想本身，离 1/2 还有一大段距离。
第二个：卡塔兰常数是无理数。
卡塔兰常数 G 的定义很简单：1 减 1/9，加 1/25，减 1/49，一直这样交替加减奇数平方的倒数。算出来大约是 0.9160。
它是不是无理数，也就是能不能写成两个整数相除，数学家问了很多年，一直没答案。
OpenAI 说证明了它是无理数，而且整个结论已经做了 Lean 形式化，题面就是上面截图里的第二段。
大家怎么看
康奈尔大学数学教授、科普作家斯托加茨（@stevenstrogatz，约 19.6 万关注）挑了矩阵乘法这一条：
Many staggering results here. But this is a particularly amazing one: the exponent for matrix multiplication is no more than 2.25. The previous world record had been something like 2.37. This leap in progress is like Bob Beamon's long jump.
这里有很多惊人的结果。其中特别了不起的一个是：矩阵乘法的指数不超过 2.25。之前的世界纪录大约是 2.37。这样的飞跃，就像鲍勃·比蒙那一跳。
@stevenstrogatz 的帖子，北京时间 10 月 7 日 6:56
鲍勃·比蒙是 1968 年奥运会跳远冠军，一跳把世界纪录提高了 55 厘米，被称为「世纪一跳」。仓库里对应的结果是 ω ≤ 9/4，并且附了 Lean 形式化。
拥有进化算法博士学位的土耳其科普作者巴克尔哲（@cagrimbakirci，约 41.9 万关注）做了个简单梳理：
Oh damn, @OpenAI just put out 722 manuscripts, grouped into 372 results across 17 fields, all produced by an internal model it hasn't named (probably "Bel"). It says the model was handed about 4,000 problems and spent around three hours of ChatGPT Pro thinking compute per…
天哪，OpenAI 刚刚放出 722 篇论文，分成 17 个领域的 372 组结果，全都出自一个还没命名的内部模型（大概叫「Bel」）。官方说模型一共接了约 4000 道题，每道平均花了约 3 小时的 ChatGPT Pro 思考算力……
@cagrimbakirci 的帖子，北京时间 10 月 7 日 6:56
模型叫「Bel」只是他的猜测，OpenAI 没有公布模型名。
最后说两句
722 篇论文，一次全放出来，数量本身就很吓人。
但数学不是看数量的。一个证明算不算数，要有人读懂、查过、能讲给别人听。
Lean 能帮上大忙，至少能确认一部分结论在逻辑上是对的。可它解决不了另一个问题：人到底能不能理解这些证明，能不能接着往下做。
顾问组那句话说得好：公开只是开始。
相关链接
• GitHub 仓库 openai/math
https://github.com/openai/math
• OpenAI 官方博客
https://openai.com/index/sharing-ai-progress-in-mathematics/
• IAS 数学与人工智能顾问组（AGMAI）
https://agmai.org/
• AGMAI 负责任发布建议（9 月 29 日）
https://agmai.org/general-sep29/
• OpenAI 关于顾问组的公告（9 月 21 日）
https://openai.com/index/advisory-group-on-mathematics-and-ai/
• OpenAI 官方帖
https://x.com/OpenAI/status/2107596713791767021
