2026年10月10日 ·34 分钟·English

七百篇手稿之后：OpenAI 数学成果的荟萃分析，与机器证明的七十年

这批手稿中有一些若被确认，将是几十年来最重要的数学进展；但截至本文写作时，没有一项经过同行评审。本文不判断这些证明的对错，而是回答三个可以核对的问题：它到底发布了什么，这些问题来自哪里，以及我们是如何走到今天的。

science

2026 年 10 月 6 日太平洋时间下午 3 点前后，GitHub 上出现了一个名为 openai/math 的新仓库。它只有一次提交，作者栏写着「Anonymous」，内容是 722 篇数学手稿、一个 Lean 形式化证明库，以及十份模型推理过程的节选（仓库 README[1]）。几十分钟后，OpenAI 发布博客与社交媒体帖子，称这是「由一个内部前沿模型产生的一批新数学结果」（OpenAI 博客[2]）。

目录里的标题读起来像一份数学界的愿望清单：拟黎曼假设、有理数域上的希尔伯特第十问题、Catalan 常数的无理性、π 的无理性指数等于 2、唯一博弈猜想、Kaplansky 的若干群环猜想、马勒猜想……当天晚上，罗格斯大学的 Alex Kontorovich 在 X 上写道：「如果是人做出了这个，那会是毫无疑问的菲尔兹奖。」（原帖[3]，据媒体转引）而同一批数学家里，也有人把它称为「一次权力的展示，而不是学术的展示」。

这篇文章想做三件事。第一，把这次发布实际包含什么、OpenAI 自己说了什么、没有说什么，尽量准确地复述一遍。第二，对 372 个结果族做一次荟萃分析：它们分布在哪些学科，结论属于证明、否定还是部分进展，原问题是哪一年提出的，有多少附带了形式化证明。第三，把这件事放回机器证明的历史里，看它在哪些意义上是新的。

需要先说明立场与局限。本文不评价任何一个具体证明是否正确，这超出了任何一篇综述的能力，也超出了目前任何一个人的能力。文中凡是 OpenAI 的说法，一律写作「声称」；凡是我们自己的归类与推断，会标明口径。

一、这次发布包含什么

规模与口径

按仓库 README 与目录文件 overview.tex 的表述，这批材料有三个层级。最底层是 722 篇手稿，每篇是一份独立的 PDF 与 LaTeX 源文件；这些手稿被归并为 372 个「结果族」（result family），一个结果族包含一个主要结果，以及它的配套论证、推论或替代证明；结果族又按学科分为 17 个类别。结果族的编号从 001 排到 377，其中 045、061、070、123、163 五个编号空缺，所以一些报道里出现的「377 个问题」其实是最大编号，不是数量。

关于生产过程，README 给出的信息只有几句：

结果由「一个未发布的 OpenAI 内部模型」产生，没有公布模型名称。
在评测过程中，模型「大约被提出了 4,000 个问题」；OpenAI 把输出聚合为结果族与手稿，并「要求达到适当的重要性水平」，最终得到这份目录。
平均每个结果使用了「相当于三小时 ChatGPT Pro 思考的算力」。
两项工作不在这一固定流程之内：黎曼 ζ 函数的零点自由区域，以及 CM 阿贝尔簇上的霍奇猜想；其中 Re(s) > 11/12 那份零点自由区域的文稿「为可读性经过人工编辑」。
README 明确提醒：「部分未形式化的结果可能存在问题。」

两点需要注意。其一，「4,000 个问题」与「372 个结果族」不能直接相除得到「成功率」，因为 OpenAI 没有公布逐题的尝试与结果，也没有说明「重要性门槛」如何设定。Scott Aaronson 在博客中给出的数字是约 8,000 个问题、约 5% 的成功率（Shtetl-Optimized[4]），与 README 不一致，我们以 README 为准。其二，「三小时 ChatGPT Pro 思考」是一个产品层面的计量单位，不对应可比较的 GPU 小时或成本，总算力与成本均未披露。

我们统计了全部 722 份 PDF 的页数，合计 34,815 页；单篇中位数 39 页，最短 6 页，最长 262 页。按结果族合计，中位数为 56 页，最长的一个结果族（时空 Penrose 不等式，编号 260）有 1,355 页。手稿目录名中的日期从 2026 年 9 月 10 日到 10 月 6 日，其中 564 篇集中在 9 月 23 日至 27 日这五天。

声称解决了什么

逐条列举 372 个结果没有意义，这里只列几项最受关注、也最便于外行理解其分量的「声称」，措辞尽量贴近目录原文：

拟黎曼假设（编号 003）：所有狄利克雷 L 函数，包括 ζ(s)，在 Re s > 7/8 的半平面内没有零点。目前已知的零点自由区域都会随虚部增大而向直线 Re s = 1 收缩，任何固定的 θ < 1 都是开放问题。
有理数域上的希尔伯特第十问题（004）：不存在算法判定任意多元整系数多项式是否有有理零点。
Catalan 常数是无理数（005），π 的无理性指数等于 2（017）。
唯一博弈猜想（102）：Khot 2002 年提出的计算复杂性猜想，目录称「证明了」它。
矩阵乘法指数 ω ≤ 9/4（107）。此前的最好上界约为 2.371。
Kaplansky 零因子猜想（196）与直接有限性猜想（197）的反例，后者同时构造了一个非 sofic 群。
自由群因子同构问题（287）：L(F₂) ≅ L(F₃)，这是算子代数中悬而未决数十年的问题。
Thompson 群 F 非顺从（248），Hadwiger 猜想的反例（157），马勒猜想（087）。

结果族与「声称」：本文把 OpenAI 目录中的每一个编号条目称为一个「结果族」。目录对每个结果族用一两句话概括其主要结论，这些概括是 OpenAI 的单方面陈述。截至 2026 年 10 月 8 日，我们没有找到任何一个结果族经过期刊同行评审，也没有找到任何一个被公开指出错误的报告。

Lean 形式化：证明了什么，没有证明什么

这次发布与以往任何一次「AI 解决数学问题」的宣布相比，最大的不同在于附带了一个规模很大的 Lean 形式化库。仓库的 lean/OAI 目录下有约 12 万个 Lean 源文件、1.7 GB 代码，使用 Lean 4.34.1 与 mathlib，并依赖二十余个外部形式化项目。

Lean 与 Comparator：Lean 是一种交互式定理证明器：数学命题被写成形式化语句，证明被写成程序，由一个很小的「内核」逐步检查每一步推理是否合法。Comparator 是 Lean 社区开发的一个核验工具：它给定一份只含命题、证明留空（sorry）的「挑战文件」，再检查某个已编译的解答是否证明了完全相同的命题，并且只用到允许的公理（通常是 propext、Quot.sound、Classical.choice 三条）。

具体来看，lean/docs 下有 235 份结果族的形式化范围说明，占 372 个结果族的 63%；清单文件 formalization.yaml 列出了 162 篇「主要结果已形式化」的手稿和 185 个主结果的 Comparator 配置；ComparatorChallenges 目录下共有 405 个挑战配置。三个数字的口径不同，不能互相替代。还有一处不一致：Catalan 常数（005）与 π 的无理性指数（017）都有范围说明和挑战文件，却不在 formalization.yaml 的清单里。

更重要的是两条限定。第一，清单的整体状态被标为 scope: "Partial progress."，审查状态为 review: status: unchecked。第二，范围说明本身经常写明形式化覆盖的边界，例如 π 那一份说「论文中关于 Flint–Hills 级数收敛的推论不在本陈述之内」，拟黎曼假设那一份说「论文后续的应用未包括在内」。

还要强调形式化证明的一个原理性边界：Lean 只能保证「这段代码证明了这个形式化命题」，不能保证这个形式化命题就是数学家心中的那个猜想。以拟黎曼假设为例，挑战文件里的命题是：

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0

这里的 riemannZeta 是 mathlib 中已有的定义，命题短到任何学过复分析的人都能读懂，因此「命题是否忠实」在这一例里几乎不成问题。但对于唯一博弈猜想这类命题，形式化陈述本身就是数百行的定义，忠实性需要专家逐行审读。

二、荟萃分析：372 个结果族

方法

数据直接取自仓库的目录文件 overview.tex（提交 adc7f12）。我们用脚本解析出每个结果族的编号、学科、标题、目录摘要、所含手稿与日期，并核对 lean/docs 下是否有对应的范围说明，用 pdfinfo 统计每份 PDF 的页数。

在此基础上，我们对每个结果族人工判读了三项信息：

原问题：它针对的是哪个已命名的猜想、问题或提问，由谁提出。
提出年份：该问题首次见诸文献或公开提出的年份，而不是后来取得部分进展的年份。无法可靠确定的，宁可留空也不估计。
结论类型：分为五类。「声称完整解决」指对原问题给出完整的肯定回答；「否定或给出反例」包括构造反例和对判定性问题给出否定回答；「部分进展」指特殊情形、条件性结果或部分参数范围；「改进界」指改进定量上界或下界但未达到猜想本身；「其他」指不以解决既有问题为框架的新定理。

判读分六批进行，主要依据数学文献与综述，对不确定的条目查阅了原始论文、erdosproblems.com、arXiv 与百科页面。完成后，我们随机抽取了 40 个已定年的条目，由独立的第二轮核查重新确定年份，40 条全部与第一轮一致；其中约十条对照了在线的原始文献或权威页面，其余依据核查者对原始文献的掌握。这说明年份大体可靠，但不意味着每一条都精确到年。完整数据表随文附在文章目录中，可以逐条核对。

几个口径问题需要事先说明。一个结果族常常同时处理几个相关问题，我们以目录标题中的首要问题为准。「结论类型」依据的是 OpenAI 的目录摘要，即它声称的结论，不代表我们认为这些结论成立。「部分进展」与「声称完整解决」之间的界线有时取决于判读者，例如一个结果族解决了某猜想剩余的全部情形，我们记为完整解决。

学科分布：几乎覆盖了整个现代数学

图 1 ｜ 372 个结果族的学科分布与结论类型。学科分类取自 OpenAI 目录，结论类型为一目半逐族判读 · 来源：openai/math 仓库目录（commit adc7f12），一目半整理与绘制

结果族最多的五个学科依次是理论计算机科学（40 个）、组合数学（37）、代数与复几何（36）、数论（31）、概率论与统计力学以及微分几何（各 29）；最少的是数理逻辑（6）。17 个学科中没有一个少于 6 个结果族，这与此前大多数「AI 做数学」的成果集中在组合与离散数学形成对比。

按结论类型，217 个结果族（58%）声称完整解决了原问题，74 个（20%）是否定或反例，53 个（14%）是部分进展，18 个（5%）是改进界，10 个（3%）是其他新结果。

一个值得注意的现象是，反例在不同学科中的比例差别很大。代数的 18 个结果族中有 8 个是反例，拓扑学 18 个中有 6 个，算子代数 19 个中有 6 个；而数论 31 个中只有 1 个，概率论与统计力学 29 个中一个也没有。一种可能的解释是，代数和拓扑中有许多「是否所有某类对象都满足某性质」形式的猜想，否定它只需构造一个对象，而构造正是搜索型系统擅长的；数论和概率中的核心问题更多是渐近估计与极限定理，很难用一个例子推翻。这是推断，没有经过检验。

年代分布：大多是 1960 至 2000 年代提出的问题

图 2 ｜可定年的 283 个结果族按原问题首次提出年代的分布，横轴标签表示该十年的起始年。浅色为 1950 年以前 · 来源：openai/math 仓库目录，一目半逐条定年并绘制

372 个结果族中，有 363 个对应一个已命名的既有问题，其中 283 个能够可靠定年。另外 80 个虽有名称，但属于数学界的「民间问题」，很难追溯到单一的首次提出，例如拟黎曼假设、Catalan 常数是否无理；还有 9 个不针对任何既有问题。

在可定年的 283 个中：

中位数是 1986 年，四分位数为 1971 年与 2004 年。也就是说，一半的问题在 1971 至 2004 年之间提出。
1960 至 1999 年提出的有 158 个，占 56%；峰值在 1970 年代（52 个）。
提出至今已满 50 年的有 97 个；1950 年以前提出的有 24 个，最早的一个是 Schläfli 1873 年关于曲面局部光滑等距嵌入的问题，此外还有 1900 年希尔伯特问题清单中的第 5、6、16 问题的相关形式。
2010 年以后提出的有 42 个，2020 年以后只有 8 个。

我们另外标记了「知名问题」，即在本学科之外也广为人知、通常有独立百科条目的猜想，共 75 个。这一标记有主观成分，仅供参考。在这 75 个中，38 个声称完整解决，23 个是否定或反例，可定年者的中位数是 1971 年，比全体早 15 年。

如何理解这个分布？一个直接的观察是，这批问题既不是新近提出、尚未被充分尝试的问题，也不以百年难题为主，而是集中在「有成熟文献、有明确表述、被一两代人尝试过」的区间。这与 OpenAI 8 月发布「Astra」十项结果时采用的筛选标准相互呼应，那次的标准是「主结果至少十年没有进展」（OpenAI[5]）。不过 README 没有公开这次的选题来源，因此我们无法判断这一分布反映的是模型的能力边界，还是选题者的偏好。

此外，17 个结果族涉及埃尔德什提出的问题。与 2025 年下半年以来 AI 与埃尔德什问题之间那一连串高度集中的故事相比，这次发布的重心明显不在这里。

形式化覆盖：与 mathlib 的成熟度高度相关

图 3 ｜各学科中附有 Lean 形式化范围说明的结果族占比，虚线为全体平均 63%。附有说明不等于主定理已被完整形式化 · 来源：openai/math 仓库 lean/docs 与目录，一目半整理与绘制

235 个结果族附有 Lean 范围说明，但各学科差别很大：数理逻辑 6/6，泛函分析 10/11，组合数学 33/37，凸几何与度量几何 13/15，群论 12/14；而数论只有 16/31，代数与复几何 7/36（19%），拓扑学 3/18（17%）。

按结论类型看，改进界的 18 个中有 17 个附有说明，否定或反例为 53/74（72%），声称完整解决为 141/217（65%），部分进展只有 18/53（34%）。

一个合理的推测是，形式化覆盖率主要取决于 mathlib 中相应理论的完备程度：组合、逻辑、初等的分析与几何已有大量基础设施，而代数几何与几何拓扑所需的概形、上同调、流形拓扑等工具在 Lean 中仍不完整。反例与定量界之所以覆盖率高，可能是因为它们往往只需验证一个具体构造，命题本身也更容易写成形式化语句。这同样是推断。

这意味着一个现实的后果：这批结果中，恰恰是数学共同体最难独立评审的那部分，比如代数几何与朗兰兹纲领方向的长篇论证，最缺少机器核验的支撑。例如 CM 阿贝尔簇的霍奇猜想（032）、虚二次域上椭圆曲线的模性（030）、有理数域上的希尔伯特第十问题（004）都没有形式化说明。

独立核验

截至 10 月 8 日，我们能找到的独立核验只针对拟黎曼假设那一条 7/8 命题。开发者 Dave Goldblatt 在一台机器上用 Comparator 复跑了这一定理，报告在 OpenAI 的配置与他自己撰写的挑战文件下均通过，所用公理只有三条标准公理（davegoldblatt/openai-zeta-proof-check[6]）。他同时列出了局限：只核验了 Lean 证明而非论文，构建过程中给依赖打了 23 个补丁，并且 OpenAI 的 405 个挑战配置中有 402 个关闭了 Comparator 的第二内核检查。另一个项目报告完成了构建与公理检查，但没有运行 Comparator。

我们也自己做了一次小规模的复核。选择的对象是结果族 049：它声称否定了 Abhyankar–Sathaye 猜想在四维及以上的超曲面形式。这个猜想预言，若多项式 F 的商环 ℂ[x₁,…,xₙ]/(F) 同构于 n−1 元多项式环，则 F 必为一个坐标，即可以通过多项式自同构变成某个变量 xᵢ。选择它有两个原因：一是它是仿射代数几何中长期开放的问题；二是它的形式化证明规模较小，只依赖 mathlib 和 15 个源文件，约 1,400 行，可以在普通机器上从源码完整重建。

我们在一个新建的 Lean 4.34.1 项目中，按仓库锁定的 mathlib 版本从源码编译了全部依赖（共 1,626 个构建任务，4 核约 17 分钟），然后做了三项检查：

把挑战文件中的命题原样抄写为一个 example，用 OpenAI 的定理去证明它，编译通过。这说明证明的确实是挑战文件中写下的命题。
用 #print axioms 检查该定理依赖的公理，结果只有 propext、Classical.choice、Quot.sound 三条标准公理，没有 sorryAx 或额外公理。
用 Lean 自带的独立检查器 leanchecker --fresh，把这一模块及其全部依赖（包括所用到的 mathlib 部分）从头送入内核重放一遍，约 5 分钟后通过，没有报错。这一步进一步排除了编译产生的中间文件出错或被改动而影响结论的可能。

这项复核只说明一件事：结果族 049 的 Lean 证明，在形式化命题的意义上是成立的。命题本身是否准确表达了 Abhyankar–Sathaye 猜想，需要代数几何学家判断；从命题的写法看，它用的是 mathlib 的标准定义，含义相当直接。它不能推广到其余 371 个结果族。

三、数学界的反应

截至本文写作时，反应可以粗略分为三类。

第一类是对结果本身的震惊。除了 Kontorovich，康奈尔大学的 Steven Strogatz 写道「这里有许多惊人的结果」，加州大学尔湾分校的 Paata Ivanisvili 写道「三维 Kakeya 拿了菲尔兹奖，四维 Kakeya 被 AI 解决了」。需要说明，目录中声称的是三维的 Kakeya 极大函数猜想和四维的 Hausdorff 维数猜想，不是整个 Kakeya 猜想。数论学家 Frank Calegari 在发布当天早些时候贴出了自己领域里的一组开放问题，发布后更新说，按他的清单打分只有「5/100」，「但另一方面仍然令人瞠目结舌」（Persiflage[7]）。

第二类是对可读性与理解的担忧。Scott Aaronson 写道，就唯一博弈猜想而言，「我们相当确信它是一个证明」，但也写道「几乎还没有任何人真正理解这些证明中的任何一个」；他转述 Dana Moshkovitz 的评价，说这篇论文写得难以卒读，「不借助 AI 几乎无法阅读」（Shtetl-Optimized[4]）。据《科学美国人》报道，OpenAI 发言人也承认，公司自己的数学家对许多结果尚不理解；MIT 的 Andrew Sutherland 的态度是：在模型公开、他人能够复现之前，「我们应该索要凭据」。以上两条为转引，我们未能直接打开原文。

第三类是对发布方式本身的批评。一个名为「人类数学协会」的团体在陶哲轩博客上发表声明，称「一次性发布 700 多份文件，不是学术的展示，而是权力的展示」（Tao 博客客座声明[8]）。这次发布前，普林斯顿高等研究院主持的「数学与 AI 咨询组」（AGMAI）曾在 9 月 29 日建议 AI 公司披露提示词、模型与逐项算力，并停止在专有模型上测试高等数学问题；OpenAI 这次没有公开提示词，也没有发布模型。咨询组在发布后表示，这是「数学的一件大事」，但其咨询角色「不应被理解为对这些结果影响的评判」（AGMAI[9]）。《自然》的新闻标题则是「数学家群情激愤」（Nature[10]）。

这些反应并不矛盾。同一个人完全可以既认为结果惊人，又认为发布方式有害。值得记录的是，截至 10 月 8 日，我们没有找到陶哲轩、Gowers、Buzzard、Scholze 等人对具体结果的公开评估；这只说明我们没有找到，不说明他们没有表态。仓库仍只有那一次初始提交，没有任何更正记录，Issue 功能处于关闭状态。

Lean 回答的是「这段推理有没有错」，同行评审回答的是「这件事值不值得、我们是否理解」。这次发布第一次让前一个问题的回答速度，远远超过了后一个。

四、机器与证明：一条七十年的时间线

图 4 ｜机器参与数学证明的主要节点，1956–2026。年份为事件公布或完成时间；2026 年的多数结果尚未经过同行评审 · 来源：各事件原始论文与官方公告，一目半整理与绘制

起点：把逻辑变成程序（1956–1970 年代）

机器证明几乎与「人工智能」这个词同时诞生。1956 年，Allen Newell、Herbert Simon 与 Cliff Shaw 的「逻辑理论家」（Logic Theorist）证明了 Whitehead 与 Russell《数学原理》第二章前 52 条定理中的 38 条，其中一条的证明比原书更短（Newell & Simon 1956, IRE Trans. Inf. Theory[11]）。逻辑理论家模仿人类的启发式搜索。两三年后，王浩走了另一条路：他在 IBM 704 上用系统的判定程序，几分钟内证明了《数学原理》中的数百条命题，包括逻辑理论家处理过的全部 52 条，并据此主张机械化的方法远比模仿人类更有效（Wang 1960, IBM J. Res. Dev.[12]）。

这两条路线的分歧，即模仿人类直觉的启发式搜索与系统化的形式推理，贯穿了此后七十年。1965 年，J. A. Robinson 提出归结原理，为一阶逻辑的自动证明提供了统一的方法（Robinson 1965, J. ACM[13]）。1967 年，N. G. de Bruijn 启动 Automath 项目，这是最早用来书写并由机器检验数学证明的语言之一；十年后，L. S. van Benthem Jutting 用它完整核验了 Landau 的《分析基础》（Automath 档案[14]）。

计算机辅助证明与「可检验性」之争（1976–2017）

1976 年，Kenneth Appel 与 Wolfgang Haken 宣布证明了四色定理。证明的关键步骤是让计算机检查近两千个可约构形，人力不可能逐一复核。这是第一次有重要定理的证明无法由人完整阅读，数学界由此争论：一个没有人能读完的证明，算不算证明？

此后的几次里程碑，在不同方向上回应了这个问题。1996 年，William McCune 的自动证明器 EQP 证明了 1933 年提出的 Robbins 猜想，这是自动定理证明器独立解决的著名开放问题（McCune 1997[15]）。1998 年，Thomas Hales 宣布用大量计算证明了开普勒猜想；《数学年刊》的审稿人在多年审查后表示「99% 确信」，但无法核对全部计算。Hales 于是发起 Flyspeck 项目，用证明助手 HOL Light 与 Isabelle 把整个证明形式化，2014 年完成，2017 年发表（Hales et al. 2017, Forum Math. Pi[16]）。

在同一时期，Georges Gonthier 等人用 Coq 完成了四色定理（2005 年）与 Feit–Thompson 奇阶定理（2012 年）的形式化证明（Gonthier 2008, Notices AMS[17]）。这些工作给出的答案是：机器参与的证明，可以由另一台机器以极高的可信度复核，而复核者只需相信一个小内核。

证明助手进入主流数学（2013–2024）

Leonardo de Moura 于 2013 年在微软研究院开始开发 Lean，社区数学库 mathlib 从 2017 年起逐步建成。转折点发生在 2020 年 12 月：Peter Scholze 公开挑战形式化社区，请他们核验他与 Dustin Clausen 凝聚态数学中一个他自己也不完全放心的定理。这个「液体张量实验」于 2022 年 7 月完成（Xena 博客[18]）。2023 年 11 月，Gowers、Green、Manners 与陶哲轩证明了多项式 Freiman–Ruzsa 猜想，社区只用约三周就把它形式化（PFR 项目[19]）。到 2024 年，陶哲轩组织的「方程理论项目」用自动证明器、人工与 Lean 协作，判定了 4,694 条原群律之间的 2,200 余万个蕴含关系。

这一阶段的意义在于：形式化证明不再只是计算机科学家的工具，而成为一线数学家愿意使用、也愿意信任的基础设施。正是这套基础设施，让今天的大模型输出可以被机器复核。

神经网络与大语言模型（2020–2025）

2020 年 9 月，OpenAI 的 GPT-f 用语言模型为 Metamath 生成证明，其中 23 个被正式收录进 Metamath 主库（Polu & Sutskever 2020[20]）。2021 年 12 月，DeepMind 与牛津、悉尼的数学家在《自然》上发表合作研究，用机器学习发现纽结不变量之间的新关系，并推动了 Kazhdan–Lusztig 多项式的组合不变性猜想（Davies et al. 2021, Nature[21]）。此后的 AlphaTensor（2022）、FunSearch（2023）用搜索发现了新的矩阵乘法算法和更大的帽集构造。

竞赛数学成为这一阶段最醒目的标尺。2024 年 1 月，AlphaGeometry 解出 30 道 IMO 几何题中的 25 道（Trinh et al. 2024, Nature[22]）；同年 7 月，AlphaProof 与 AlphaGeometry 2 在 IMO 2024 上得到 28/42 分，达到银牌水平，但题目需要人工翻译为 Lean，部分题目耗时三天。2025 年 7 月，OpenAI 的实验模型与 Google 的 Gemini Deep Think 都在 IMO 2025 上以自然语言作答达到 35/42 分的金牌线，后者经过 IMO 官方评分；Harmonic 的 Aristotle 与字节跳动的 Seed-Prover 则给出了五道题的 Lean 形式化解答。

研究层面的评测随之出现。2024 年 11 月，Epoch AI 发布 FrontierMath，当时最好的模型解出不到 2%（Glazer et al. 2024[23]）。2025 年 5 月，DeepMind 的 AlphaEvolve 找到了用 48 次乘法计算 4×4 复矩阵乘积的算法，改进了 Strassen 1969 年以来的 49 次。

2025 年 10 月发生了一次值得记住的失误。OpenAI 的一位副总裁发帖称 GPT-5「找到了 10 个此前未解的埃尔德什问题的解」，埃尔德什问题网站维护者 Thomas Bloom 随即指出这是「严重的误导」：这些问题在网站上标为「开放」，只是因为他本人不知道已有解答，GPT-5 找到的是现有文献。帖子随后被删除（TechCrunch[24]）。此后几个月，确实出现了 AI 实质参与的埃尔德什问题进展，例如 2025 年 12 月第 1026 号问题由 Aristotle、AlphaEvolve、文献检索与多位数学家合作解决，陶哲轩详细记录了过程（Tao 博客[25]）。陶哲轩等人随后维护了一个「AI 对埃尔德什问题的贡献」维基，按完整、部分、错误、仅找到文献等类别逐条记录（GitHub wiki[26]）。这种分类方法，也是本文荟萃分析的参照之一。

2026 年：从单点突破到批量生产

2026 年的节奏明显加快。按时间顺序，以下是与本文主题直接相关的事件。

2 月：Abouzaid、Hairer、Srivastava 等 11 位数学家发布「First Proof」，用 10 道未发表的研究级问题测试 AI（arXiv:2602.05192[27]）。OpenAI 声称其中至少 5 道「可能正确」，同时承认有人工引导（OpenAI[28]）；DeepMind 的 Aletheia 被专家多数判定解出 6 道（arXiv:2602.21201[29]）。
5 月 20 日：OpenAI 宣布其内部模型否定了埃尔德什 1946 年的单位距离猜想，即证明存在无穷多个 n，使平面上 n 个点之间至少有 n^(1+δ) 对单位距离。这一结果经过一组外部数学家核查，Gowers 称之为「AI 数学的里程碑」，Jacob Tsimerman 表示会「毫不犹豫地」接受它发表（OpenAI[30]）。
6 月 2 日：一组数学家发表《莱顿宣言》，国际数学联盟予以认可，强调 AI 是工具而非作者，并列出不可靠、署名、专有依赖、炒作与自主性五类风险（Leiden Declaration[31]）。
7 月 19 日：Anthropic 的研究者 Levent Alpöge 公布了一个三维雅可比猜想的反例，该猜想由 Keller 于 1939 年提出。反例是一个可以直接用计算机代数验证的 7 次多项式映射。Alpöge 在社交媒体上把它归功于 Anthropic 的模型；随后 Shuhong Gao 把构造推广到所有大于 2 的维数（arXiv:2608.00222[32]），二维情形仍然开放。
8 月：OpenAI 发布「Astra」的十项结果，每项附 Lean 证书（OpenAI[5]）。Anthropic 宣布其未发布模型把已证明位于临界线上的 ζ 零点比例下界从 41.6% 提高到 67.2%，附 Lean 证明，并明确这与证明黎曼假设无关（Anthropic[33]）。
9 月 8 日：OpenAI 声称其多智能体系统证明了 Clay 千禧年问题中 Navier–Stokes 方程的「爆破」方向，即带光滑外力时存在有限时间爆破，并附 Lean 形式化，同时表示不申领奖金（OpenAI[34]）。Clay 研究所尚未认定，此事还伴随着与 Alpöge 和 Tristan Buckmaster 的优先权争议。
9 月 11 日：28 位菲尔兹奖得主联署《AI 在数学中的严重错位》，批评 AI 公司把数学问题当作基准测试，成果「仓促宣布、来不及撰写规范的文稿」，并引发「严重的署名与剽窃问题」（mathandai.org[35]）。
9 月下旬：普林斯顿高等研究院成立独立的数学与 AI 咨询组（AGMAI），成员包括 Gowers、Hairer、Witten 等九人，其成立后的首要工作之一，就是就 OpenAI 的这次大规模发布提供建议。
10 月 6 日：本文讨论的 722 篇手稿公开。

对上面各家公司的公告，我们采用同样的标准：只陈述公告内容与已知的外部核查情况。

五、几点思考

证明的生产、验证与理解正在分离

在过去，一个定理的证明、验证与理解通常由同一群人在同一过程中完成：证明者写出论证，审稿人读懂并确认，同行在阅读中吸收其中的思想。四色定理第一次把「验证」从这个过程中部分剥离出来，交给了机器；形式化数学让这种剥离变得可信。

这次发布把剥离推向了第三个环节。34,815 页手稿，即使按一位专家每天仔细读 20 页估算，也需要近 1,750 个工作日。更关键的是，Aaronson 和 Moshkovitz 的评论表明，即使证明是对的，其中的思想也未必能被人类顺利吸收。这引出一个过去只在哲学讨论中出现的问题：如果一个定理被机器证明、被机器验证，却没有人理解，它在什么意义上成为了「数学知识」？

验证的瓶颈移到了「命题是否忠实」

Lean 让「证明有没有错」这个问题变得可以机械地回答，但它把压力转移到了另一个地方：形式化命题是否准确表达了原猜想。对于拟黎曼假设这样短小的命题，这一点很容易检查；对于唯一博弈猜想、霍奇猜想这类需要大量定义才能陈述的命题，审读形式化陈述本身就是一项专业工作。此外，如前所述，最需要机器核验的那些学科，恰恰是形式化基础设施最薄弱的学科。

规范的建立落后于能力的增长

从《莱顿宣言》、菲尔兹奖得主联署到 AGMAI 的指导意见，数学共同体在 2026 年用了很大力气讨论规范：署名、披露、复现、节奏。这次发布在形式上回应了其中一部分，比如征询了 AGMAI、附带了形式化证明、承诺保留版本历史；但在提示词、模型可得性与发布节奏上没有采纳建议。一个可以预见的后果是，接下来几个月，许多数学家的工作将被迫从「证明新定理」转向「审读 AI 的定理」，而这部分劳动目前没有明确的归属与回报。

对 AI 与生命科学交叉领域的读者

这个专栏的许多读者在 AI 与生命科学的交叉处工作。数学是 AI 最容易「自我验证」的领域：有严格的形式语言、有可以机械检查的证明。即便如此，这次发布暴露出的问题，比如验证覆盖不均、命题忠实性、人类理解跟不上、发布节奏压垮评审能力，都在数学中真实存在。生物学既没有 Lean，也没有一个小内核能保证结论无误，实验验证又慢又贵。可以合理推测，当 AI 在生物学中开始批量产出「发现」时，这些问题只会更严重。数学界在 2026 年建立的规范，或许值得生命科学提前借鉴。

结论与仍然开放的问题

回到开头。OpenAI 这次发布的，是一个内部模型在大约 4,000 个问题上运行后，经过筛选的 372 个结果族、722 篇手稿。按我们的整理，其中 58% 声称完整解决了原问题，20% 给出否定或反例；原问题的提出年份中位数为 1986 年，集中在 1971 到 2004 年；63% 的结果族附有 Lean 形式化说明，但覆盖率在组合与逻辑中很高，在代数几何与拓扑中很低。截至 10 月 8 日，没有一项结果经过同行评审，也没有一项被指出错误。

这个梳理有几处局限。第一，结论类型依据的是 OpenAI 的目录摘要，不代表结论成立。第二，问题的提出年份主要依据文献记载与我们的判读，抽样核查一致，但不排除个别条目有数年误差，另有 89 个结果族无法可靠定年。第三，「知名问题」的标记有主观成分。第四，我们只能看到被筛选后公开的结果，看不到其余约 3,600 个问题上发生了什么，因此本文的任何比例都不能解读为模型的成功率。

要点

OpenAI 于 2026 年 10 月 6 日公开 722 篇数学手稿、372 个结果族，由一个未公开名称的内部模型在约 4,000 个问题上产生，平均每个结果约相当于三小时 ChatGPT Pro 的思考算力；手稿合计 34,815 页。
按一目半逐族整理：58% 声称完整解决原问题，20% 为否定或反例；可定年的 283 个问题提出年份中位数为 1986 年，1950 年前提出的有 24 个；反例在代数、拓扑与算子代数中比例最高，在数论与概率中几乎没有。
63% 的结果族附有 Lean 形式化说明，但仓库整体状态为「部分进展、未核查」，且覆盖率在代数几何与拓扑中最低；截至 10 月 8 日，独立的形式化复核只覆盖了极少数命题，没有任何结果经过同行评审。
从 1956 年的逻辑理论家到 2026 年的批量发布，机器先接管了搜索，再接管了验证；这次发布显示，证明的产出速度已经远远超过人类理解与评审的速度。

仍然开放的问题至少有三个。其一，这批结果中有多少会在细读后被确认，又有多少需要修正？OpenAI 承诺记录更正，这会是检验其可靠性的第一份真实数据。其二，当一个证明经过机器验证却无人理解，数学共同体应当如何对待它：接受它、引用它，还是等待一个人类可读的版本？其三，选题本身是否会改变：当「被提出了几十年、有清晰表述的问题」可以被批量解决，数学家会把精力转向提出问题、建立理论与解释结果吗？这三个问题的答案，大概要在未来一两年里才能逐渐看清。

数据与方法说明：本文荟萃分析的完整数据表为文章目录下的 openai-math-families.csv，每行一个结果族，字段包括学科、标题、原问题、提出者、提出年份及依据、年份可信度、结论类型、是否为埃尔德什问题、是否为知名问题、手稿数与总页数、手稿日期范围、是否附有 Lean 范围说明、抽样复核结果，以及 OpenAI 的目录摘要原文。数据来源为 openai/math[1] 仓库提交 adc7f1241b42e322a6451854ab7e4b4c146bf78a。所有图表由一目半根据上述数据绘制。