编辑｜Panda
今天上午，OpenAI 把一个尚未发布的内部模型产出的 722 篇数学手稿一次性放上了 GitHub。发布本身的来龙去脉、模型背景和数学界的争议，我们在上一篇报道里已经梳理过。这一篇换个角度，打开仓库，看看清单上到底有哪些成果。
仓库地址：https://github.com/openai/math
首先，有必要进行一些说明：
第一，这 722 篇手稿被归入 372 个「成果族」，覆盖数论、几何、理论计算机、数学物理等 17 个方向，本文按方向挑出其中名气最大、牵涉问题最古老的一批来介绍。
第二，清单里既有「证明」也有「证伪」，按我们的粗略检索，摘要中出现「证伪」「反例」字样的成果族约有 50 个，一些流传了半个多世纪的猜想是被推翻而不是被证明的。
第三，也是最重要的一点：下文所有「证明了」「解决了」都是 OpenAI 自己的表述，绝大多数尚未经过同行评审。其中约六成成果族附有 Lean 形式化，即由计算机逐行检查过的证明，我们会在提到时注明；没有形式化的结果，目前只能算「声称」。
数论：从黎曼到希尔伯特
数论是这份清单里最惊人的部分，31 个成果族中有好几项直接挂着史上最著名的名字。
排在仓库第 003 号的准黎曼猜想，是传播最广的之一。黎曼在 1859 年提出，zeta 函数的非平凡零点全部落在一条竖线上；这个终极目标太远，数学家退而求其次，希望至少证明某条竖线右边干干净净、一个零点都没有。一百多年里，这件事始终没有做成。OpenAI 声称把这条线划在了 7/8 的位置，对 zeta 函数和所有狄利克雷 L 函数同时成立，并附上了 Lean 形式化。
准黎曼猜想
与黎曼猜想同列千禧年大奖难题的 BSD 猜想，也出现在清单上。它讨论的是椭圆曲线上有理点的多少，与一个解析函数在某一点的行为之间存在精确对应。OpenAI 的第 002 和 006 号成果族合在一起，声称对每一条有理椭圆曲线，在它「几乎所有」的二次扭曲上都证明了完整的 BSD 公式；其中 006 号还顺带证明了数论学家 Dorian Goldfeld 在 1979 年提出的 Goldfeld 猜想。这两项都没有形式化。
BSD 公式
Goldfeld 猜想
第 004 号指向的是 1900 年希尔伯特提出的 23 个问题中的第十个。原问题问的是：有没有一种通用算法，能判断任意一个整系数多项式方程是否有整数解？1970 年，Yuri Matiyasevich 在前人工作基础上给出了否定回答。但如果把「整数解」换成「有理数解」，问题就悬置了半个多世纪。OpenAI 声称这一版本的答案同样是否定的，这一项同样没有形式化。
希尔伯特第十问题（有理数域）
还有两项结果，普通读者也能一眼看懂题面。
一是卡塔兰常数，也就是 1 减 1/9 加 1/25 减 1/49 如此交替下去的那个和，它是不是无理数一直没人知道；OpenAI 声称它是。
卡塔兰常数
二是圆周率 π 「有多难被分数逼近」：此前数学家能证明的上界大约是 7.1，OpenAI 声称最优值恰好是 2，也就是说 π 在这件事上和「绝大多数」无理数一样普通。后者还顺带解决了一道趣味数学界流传多年的问题，即所谓 Flint Hills 级数是否收敛。这两项都附有 Lean 形式化。
π 的无理性测度
代数几何：霍奇猜想的一角，与有理性之谜
代数与复几何以 36 个成果族排在第三。这里最醒目的是第 032 号：对所有复 CM 阿贝尔簇证明有理霍奇猜想。霍奇猜想是千禧年大奖难题之一，大意是某些「拓扑上看起来像几何对象」的东西，一定真的能由代数方程切出来。CM 阿贝尔簇是一类对称性极强的特殊对象，远不是全部情形，但 OpenAI 称借助 James Milne 此前的定理，这一结果还能推出有限域上所有阿贝尔簇的 Tate 猜想。仓库 README 也特意注明，这一项没有走模型的标准流程，且目前没有形式化。
CM 阿贝尔簇霍奇猜想
另一项值得留意的是第 054 号。三次四维簇能否被有理参数化，是代数几何里出了名的难题，Alexander Kuznetsov 曾提出一个用「范畴」语言判断的猜想。OpenAI 声称构造出了满足这一判据、却依然不能有理参数化的例子，从而推翻了该猜想。
三次四维簇（Kuznetsov 猜想反例）
再往抽象处走，清单里还有第 069 号的量子几何朗兰兹对应。2024 年，Dennis Gaitsgory 等人以近千页的系列论文证明了几何朗兰兹猜想，OpenAI 声称把其「量子」版本在无理参数下也做了出来。
量子几何朗兰兹
第 008 号则声称解决了关于 Grothendieck–Teichmüller 李代数结构的 Deligne–Drinfeld 猜想，并附有 Lean 形式化。
Deligne–Drinfeld 猜想
分析与几何：挂谷、马勒和一百年前的猜想
几何与分析方向的名题同样密集。
挂谷问题（第 074 号）起源于 1917 年日本数学家挂谷宗一的一个小问题：一根针要在平面上转一整圈，最少需要扫过多大面积？它的高维版本演变成调和分析的核心难题之一。今年 7 月，王虹凭借与 Joshua Zahl 合作证明三维挂谷集合猜想获得菲尔兹奖；OpenAI 声称在此基础上更进一步，证明了三维的更强版本和四维的维数猜想。这一项没有形式化，也是最需要专家尽快审读的成果之一。
三维挂谷极大猜想
四维挂谷
马勒猜想（第 087 号）由 Kurt Mahler 在 1939 年提出，问的是一个凸体与它的「对偶体」体积乘积最小能有多小，直到 2020 年才有日本数学家解决了三维对称情形。OpenAI 声称在所有维数上同时解决了对称与非对称两个版本，并刻画了所有取到最小值的情形，附有 Lean 形式化。
马勒猜想（对称）
马勒猜想（一般凸体）
第 071 号回到了更古老的年代。1908 年，Paul Koebe 猜想平面上任何区域都可以通过保角变换，变成边界全是圆或点的「圆域」。OpenAI 声称解决了这一猜想的存在性部分，附有 Lean 形式化。
Koebe 圆域猜想
几何方向的其他亮点还包括：任意黎曼度量下的高维球面都有无穷多条闭测地线（第 345 号），以及度量版 Blaschke 猜想（第 344 号），这两项目前都没有形式化。
球面上无穷多闭测地线
度量 Blaschke 猜想
理论计算机：唯一游戏猜想落地
理论计算机科学是整个仓库里成果族最多的方向，一共 40 个。其中分量最重的是第 102 号：唯一游戏猜想。
这个猜想由 Subhash Khot 在 2002 年提出，Khot 后来因此获得 2014 年奈望林纳奖。它的意义在于，如果猜想成立，一大批经典优化问题，比如把图的顶点分成两组、让组间连边尽量多的 Max-Cut 问题，其「最好能近似到什么程度」都会被一锤定音。2018 年，Khot 与合作者证明了其较弱的「2 对 2」版本，但完整猜想一直悬而未决。OpenAI 声称给出了完整证明，并直接推出 Max-Cut、顶点覆盖等问题的最优近似门槛，主结果附有 Lean 形式化。
唯一游戏猜想
同一方向的第 106 号也值得一提：对于一张已知能用三种颜色着色的图，用任何固定数量的颜色去给它着色都是 NP 困难的。这道题看起来简单，却困扰了理论计算机科学界数十年，同样附有 Lean 形式化。
三色可着色图的着色困难性
组合与图论：一个经典猜想被推翻
组合数学有 37 个成果族，其中最出人意料的一项是第 157 号：推翻 Hadwiger 猜想。
Hadwiger 猜想由 Hugo Hadwiger 在 1943 年提出，是著名的四色定理的推广，长期被视为图论中最重要的开放问题之一，此前只在小规模情形下被证明成立。OpenAI 声称构造出了任意大的反例，而且是在比原猜想更弱的「分数着色」版本下就已经不成立，附有 Lean 形式化。如果这一结果经得起检验，它在图论界的冲击力可能不亚于任何一项证明。
Hadwiger 猜想反例
另一项与着色有关的成果是第 158 号：平面不能只用五种颜色完成「距离为 1 的两点不同色」的染色。这就是著名的平面染色数问题。几十年来，答案一直被夹在 4 到 7 之间，2018 年 Aubrey de Grey 借助计算机把下界提到 5；OpenAI 声称再提到 6，于是只剩 6 和 7 两种可能，附有 Lean 形式化。
平面染色数至少为 6
第 159 号则关乎埃尔德什最著名的猜想之一：如果一组正整数的倒数之和发散，那么其中一定包含任意长的等差数列。2004 年，Ben Green 与陶哲轩证明了素数中有任意长的等差数列，这正是该猜想的一个特例；埃尔德什生前曾为其悬赏 5000 美元。OpenAI 声称证明了猜想本身，附有 Lean 形式化。
埃尔德什等差数列猜想
此外，第 179 号还声称解决了 Herbert Ryser 在 1963 年提出的循环 Hadamard 矩阵猜想。
循环 Hadamard 矩阵猜想
代数与算子代数：一连串「反例」
如果说其他方向以证明为主，那么代数和算子代数方向则以证伪居多。
Irving Kaplansky 在上世纪中叶提出了一组关于群代数的猜想，其中「单位猜想」已在 2021 年被 Giles Gardam 用计算机辅助搜索出的反例推翻。这一次，OpenAI 在第 196 号中声称推翻了同组里的零因子猜想，在第 197 号中推翻了直接有限性猜想，均附有 Lean 形式化；第 294 号还推翻了 Kaplansky 关于 C* 代数中拟迹的另一个猜想。
Kaplansky 零因子猜想反例
Kaplansky 直接有限性猜想反例
Kaplansky 拟迹猜想反例
第 285 号的分量更重：它声称给出了无系数版 Baum–Connes 猜想的反例，并同时推翻 Kadison–Kaplansky 猜想。Baum–Connes 猜想自 1982 年提出以来，是连接几何、拓扑与算子代数的枢纽性猜想，此前已知的反例都需要额外条件。这一项目前没有形式化。
Baum–Connes 猜想反例
Kadison–Kaplansky 猜想反例
同一方向唯一一项「正面」结果却同样重磅。第 287 号声称解决了自由群因子同构问题：不同数量生成元的自由群所对应的冯·诺依曼代数，到底是不是同一个东西。这是算子代数领域最著名的未解问题之一，OpenAI 给出的答案是「全部同构」，附有 Lean 形式化。
自由群因子同构
数学物理：给物理学家的直觉补上证明
数学物理与概率统计力学两个方向合计 54 个成果族，这里的很多结论物理学家早就「相信」，只是缺少严格证明。
第 268 号声称证明了 Haldane 猜想：自旋为 1 的反铁磁海森堡链存在能隙。这一预言由 Duncan Haldane 在 1983 年提出，是他获得 2016 年诺贝尔物理学奖的工作之一。
Haldane 能隙
第 271 号则声称严格证明了 Felix Bloch 在 1930 年提出的铁磁体低温磁化 T 的 3/2 次方定律，并给出精确系数。
Bloch 定律
第 216 号关注的 BKT 相变，同样是 2016 年诺贝尔物理学奖的主题；第 221 号的 Mézard–Parisi 公式，则与 2021 年诺贝尔物理学奖得主 Giorgio Parisi 的自旋玻璃理论有关。
BKT 普适性
Mézard–Parisi 公式
第 215 号声称构造了二维 O(3) 模型的连续极限，并证明其存在正的质量间隙，附有 Lean 形式化。这个模型常被视为杨-米尔斯理论的「玩具版」，后者的质量间隙问题本身就是千禧年大奖难题之一。
二维 O(3) 模型质量间隙
流体方向也有惊喜。除了 9 月已经公布的 Navier-Stokes 奇点结果，仓库第 376 号声称构造出一种在外力驱动下能够执行任意图灵机程序的 Navier-Stokes 流体，也就是「用流体做通用计算」，附有 Lean 形式化。陶哲轩曾在 2016 年设想，用流体搭建「计算机」或许是理解 Navier-Stokes 方程奇点的一条路径。
Navier-Stokes 流体通用计算
第 362 号则声称证明了三维相对论 Vlasov–Maxwell 方程组在大初值下的整体光滑解，附有 Lean 形式化。
相对论 Vlasov–Maxwell 整体光滑解
写在最后
把这份清单从头翻到尾，最直观的感受是「密度」。一个研究生在一个子领域里能叫出名字的经典问题，往往只有一两个，而这里在每个方向都排了好几个。很多问题的年龄比提出它们的数学家还要长。
但密度也是这份清单最需要冷静对待的地方。社交媒体上最热的几项，四维挂谷、霍奇猜想的 CM 情形、有理数域上的希尔伯特第十问题、Baum–Connes 反例，恰好都还没有 Lean 形式化。即便是已经形式化的结果，形式化证明是否忠实对应了猜想的原始表述，仍需要专家逐一确认。按照数学界的惯例，单是其中任何一项被学界真正接纳，都可能需要数月乃至数年。正如 OpenAI CEO Sam Altman 引述之诗描写的那样：「沧海辽阔，而我的船如此渺小。」
清单已经公开在那里。接下来的问题，是 722 篇手稿里有多少能经受住检验，而数学家们又需要多久才能读完它们。
