OpenAI 在官方发布文章中公布了一批由内部前沿模型生成的数学研究成果。GitHub 成果库包含 722 篇手稿，归为 372 个相关成果家族，涉及数论、几何、数学物理与理论计算机科学等领域。

这些手稿提出的推进，已经具体到长期未解问题的答案与证明路线。 例如，把圆周率 π 的分数逼近指数确定为 2，证明三维相对论等离子体方程在规定的大初值条件下始终光滑，构造 ab = 1 却 ba ≠ 1 的代数反例，以及去掉最大割近似困难性结果所依赖的额外猜想。它们分别在追问：分数能贴近 π 到什么程度、方程会不会在有限时间内失控、一个经典猜想是否成立，以及快速算法的保证能有多好。

这批结论处于不同验证阶段；722 篇手稿也不代表独立解决了 722 个问题。此次公开同时提供了部分命题的 Lean 形式化代码和 10 份推理过程摘要，让外界能够检查论文、推导与探索过程。下面先看具体数学推进，再看它们怎样产生、目前能核查到哪一步。

六个例子，看懂这些数学结论在回答什么

下面的六个例子涵盖猜想的证明、否定猜想的反例与算法的理论极限。有些新结果还被用于下一项研究，形成了可以继续追踪的推导链条。

1. 拟黎曼猜想：排除一片区域，仍不等于找到所有零点（家族 003）

黎曼猜想是著名的千禧年数学难题之一，核心关乎素数的分布规律。猜想断言黎曼 ζ 函数的所有非平凡零点都位于复平面实部等于 1/2 的直线上（其中 Re(s) 表示复数 s 的实部）。因为直接证明这条直线极其困难，数论中退而研究条件较弱的“拟黎曼猜想”：能否在复平面右侧证明存在某个常数 θ < 1，使得半平面 Re(s) > θ 内完全不存在零点。

在成果库的家族 003 中，主论文宣称对所有狄利克雷 L 函数（包括黎曼 ζ 函数）以及特定虚二次域上的有限阶赫克 L 函数，证明了在半平面 Re(s) > 7/8 内没有零点（允许 s=1 处的极点）；同家族另一篇论文则给出了 Re(s) > 11/12 的备选证明。从数学区域来看，7/8 比 11/12 更靠近 1/2，因而排除零点的范围更大，它没有排除 1/2 < Re(s) ≤ 7/8 之间的零点，也就没有证明所有非平凡零点都在 1/2 线上。

只画复数的实部方向；这是结论范围的示意，没有绘制实际零点。

01/27/81 Re(s)：复数的实部

黎曼猜想的要求
所有非平凡零点都落在 Re(s) = 1/2。

此次稿件的主张
Re(s) > 7/8 的区域没有零点。

7/8 = 0.875。排除右侧区域，仍没有把中间区间的零点全部定位到 1/2；图中的斜纹区域也不表示零点数量或完成比例。

该家族同时给出了关于朗道-西格尔实零点（贴近 1 的潜在实零点）的均匀排除结果。在配套的 Lean 形式化代码中，团队形式化了 Re(s) > 7/8 的无零点结论以及对数排斥边界；其中排斥界的正常数没有给出显式数值；论文后续应用也不在这些选定的形式化声明范围内。

2. 圆周率的逼近极限：分数能把 π 逼近到什么程度？（家族 017）

数学界早在一个多世纪前就已经证明 π 是无理数，这项研究既不是为了证明 π 的无理性，也不是提出计算圆周率小数位的新算法，而是探究用有理分数逼近 π 的精度极限。在数论中，“无理数指数”用来刻画这种逼近难度：分母为 q 的分数 p/q 靠近目标无理数时，误差能小到什么程度。根据狄利克雷逼近定理，任何无理数的逼近指数至少为 2；若指数恰好为 2，意味着对任意给定的 ε > 0，只要分母 q 足够大，误差就不可能低于 1/q^2+ε，即分数无法以更高的阶数超常贴近该数。

达到 2 的意义，是把这个指数的上界与下界合上。 狄利克雷定理已保证它不小于 2；若能再证明它不大于 2，就能确定精确数值，而不只是缩小可能范围。这正是该稿件声称完成的推进。

家族 017 的论文声称给出了 π 的无理数指数恰好等于 2 的证明，并由此推导了经典弗林特-希尔斯级数（Flint–Hills series）的收敛性： 1/(1³ sin²1) + 1/(2³ sin²2) + 1/(3³ sin²3) + …

在这个级数中，每一项都是正数；由于正整数 n 是以弧度参与计算，一旦 n 恰好非常接近 π 的某个整数倍，|sin n| 就会变得极小，使得该项数值急剧增大。这个级数能否累加出一个有限的求和结果，取决于分母上的 n^3 是否足以压制住这些骤然膨胀的项。限制有理数对 π 的逼近程度，有助于为这些异常大项设定增长上限。不过，无理数指数给出的渐近下界并不能直接生搬硬套成对所有正整数 n 的简单逐项估计，级数的收敛性是论文通过后续深入推导得出的结论。配套的 Lean 范围说明 覆盖“π 的无理数指数等于 2”这一核心命题；弗林特-希尔斯级数的收敛性在 Main.lean 中已有推论代码，但未列入这个 Comparator 配置 的选择范围。

3. 相对论等离子体系统：大初始状态能否一直平滑演化？（家族 362）

在偏微分方程领域，相对论性弗拉索夫-麦克斯韦系统（Relativistic Vlasov–Maxwell system）用于描述带电粒子群与其自洽产生的电磁场之间的非线性耦合演化。与宏观流体速度场不同，该方程直接刻画粒子在位置和动量构成的相空间中的分布演化。在狭义相对论框架下，单个粒子的运动速度天然受到光速限制；数学上核心问题在于：在没有微小扰动、几何对称或电中性等简化假设的前提下，若赋予系统任意大的平滑初始状态，非线性场与粒子分布的相互作用是否会在有限时间内失控，导致场的导数发散或解丧失光滑性。

家族 362 的论文针对三维单物种相对论弗拉索夫-麦克斯韦系统的大初值问题提出了整体经典解的存在性与唯一性证明。在设定的初值条件下，初始粒子密度在相空间中非负、光滑且具有紧支撑（即粒子局限在有限的空间和动量区域内），初始电磁场具有有限总能量、各阶空间导数有界并满足麦克斯韦方程组的高斯约束（保证初始电磁场与电荷分布相容的条件）。论文得出结论：该系统在任意有限时间区间内始终保持光滑解，且粒子在相空间中的支撑始终保持紧致，从而排除了有限时间内奇点的产生。

速度有上限，动量却仍可能无限增大。 在论文采用的归一化单位中，动量 v 对应的速度是 u = v / √(1 + |v|²)：动量越大，速度越接近光速，却始终不越过光速。因此，光速限制本身不能保证解一直光滑。此前已有大初值整体弱解，但弱解不提供这里要求的光滑性与唯一性；不少经典解成果则依赖小初值、低维或对称性。该稿件主张推进到三维、任意符合上述条件的大初值，且不要求对称性。动量在每个有限时间区间内有界，仍允许它随时间增长。

原论文的证明路线围绕“怎样阻止动量在有限时间内变得无限大”展开。先沿粒子轨道累加带方向的电磁力，再计算净冲量的大小，可以保留方向相反的贡献之间的抵消；若每一刻都只取力的大小再累加，这些抵消就丢失了。论文结合粒子的方向变化、在危险角向区域停留的时间与误差控制，建立净冲量估计，再推出最大动量每翻一倍所需的时间下界。这些时间下界的总和发散：即使每次翻倍越来越快，也无法把无限次翻倍挤进有限时间。于是，有限时间内动量保持有界，配合匹配初值条件的延拓判据，让经典解继续演化。这是论文提出的论证路线，关键在新的估计能否成立。

该项数学结论在 Lean 库中提供了针对大初值经典解整体存在性与唯一性的形式化命题。这项结论回答的是：在这个方程模型与规定的初值条件下，大规模初态能否持续得到唯一、光滑的演化，但它建立在理想化的单物种与特定初值条件之上，并不等同于真实复杂物理环境中的等离子体在所有工况下都不会发生不稳定性或突变。

4. 霍奇猜想的特定情形：把几何信息对应到代数方程（家族 032）

霍奇猜想要连接几何空间的两种描述：一边是空间的整体几何与拓扑信息，另一边是代数方程定义出的几何子空间。在光滑射影复代数簇上，上同调群记录几何与拓扑信息；其中满足特定复结构条件的有理上同调类，称为“有理霍奇类”。猜想追问：这些类是否都能表示为代数循环的上同调类的有理线性组合？（代数循环由代数方程定义的几何子簇组合而成。）如果成立，就能把这些霍奇类对应到由方程定义的几何对象上。

一般猜想面向所有光滑射影复代数簇。这批稿件针对的是特定对象：即使在所研究的对象上覆盖了任意维度与余维度，也仍然需要区分“这一类对象全部成立”和“所有对象都成立”。

家族 032 包含 8 篇论文，主要攻关目标集中在两类特定的经典几何对象上：一是在任意维度与余维度上证明了所有具有复乘结构（Complex Multiplication，简称 CM）的复阿贝尔簇的有理霍奇猜想，并由此关联推导出有限域上阿贝尔簇的泰特猜想等推论；二是证明了任意射影复 K3 曲面有限积上的有理霍奇猜想，以及这类曲面上库加-佐武（Kuga–Satake）对应的代数性。这些成果针对的是特定的几何簇类，并非解决了适用于任意光滑射影簇的完整霍奇猜想。

值得注意的是，OpenAI 在仓库说明中指出，复乘阿贝尔簇霍奇猜想这项工作属于固定流程之外的例外；这也说明不能把整批成果都当成完全相同条件下的评测输出。

5. 群代数直接有限性：乘积顺序不可随意颠倒的反例（家族 197）

在普通的算术与数系中，如果两个数满足 a × b = 1，那么交换顺序后 b × a 也必然等于 1。但在抽象代数的群代数结构中，元素的乘法未必能交换顺序。著名的卡普兰斯基（Kaplansky）直接有限性猜想曾推测：在任意域与任意群构成的群代数中，只要 ab = 1 成立，就一定能推出 ba = 1，即这类代数系统均保持某种类似有限维代数的良好性质。

家族 197 针对这一猜想给出了否定性回答。论文在特征二的有限域上构造出了具体的群代数反例，找到满足 ab = 1 却导致 ba ≠ 1 的代数元素；配套的 Lean 形式化代码 包含了有限生成群与带奇素数阶元有限呈现群下的反例陈述。在数学研究中，构造反例推翻流传数十年的猜想与直接证明定理同样是实质性的研究进展；这并不意味着日常熟悉的普通数算术法则发生了改变，而是为非交换代数结构划定了严格的有效边界。

这个反例还被用于下一项研究。摘要第二部分以同一组 ab = 1、ba ≠ 1 的元素为输入，构造无限群上的细胞自动机：每个位置取有限种状态，新状态只由有限邻域决定，各处使用同一规则。先执行变换 b、再执行 a 能复原输入（Ta ∘ Tb = id），所以 b 不会把两个不同输入变成同一输出，这叫单射；ba ≠ 1 则给出某个永远无法由 b 产生的输出，使它不是满射。这里考虑的是无限整体配置。后续推导依赖前述代数反例，从它导出了新的结果，并没有重新独立证明那个反例。

6. 最大割近似阈值：确定性算法的效率极限（家族 102）

最大割问题（Max-Cut）要求把图里的顶点分成两组，让跨越两组的连线尽量多。由于精确求出最优割是 NP-难问题，算法设计转向快速寻找近似解。高曼斯-威廉姆森（Goemans–Williamson）算法的理想近似比率 α_GW ≈ 0.878567，约为 87.86%。比率比较的是算法得到的割与这张图的最优割，不是全图的连线总数。该算法用随机超平面得到期望保证，有限精度实现可以任意接近这一比率；例如最优割有 1000 条边时，这相当于接近 879 条边的期望保证，并不限制某次运行取得更好的结果。

这项工作的关键新意，在于改变了困难性结论所依赖的假设。经典的最优困难性结果需要“唯一博弈猜想”（Unique Games Conjecture，UGC）这一额外假设；本论文主张去掉它，证明在简单无权图上，任何大于 α_GW、不超过 1 的固定近似比率都是普通 NP-难的。它试图说明：这个阈值限制的不只是某种特定算法，而是通用近似算法能提供的最坏情况保证。

论文与配套的 Lean 形式化结果给出了从二进制 3SAT 到最大割间隙判定的确定性多项式时间转换（3SAT 判断一组布尔逻辑条件能否同时满足；它是 NP-完全问题，转换时间由输入规模的固定次幂控制）。如果通用确定性近似算法能始终超过上述阈值，就可用这个转换在多项式时间内判定 3SAT。因此，在 P ≠ NP 的假设下，这样的算法不存在。去掉 UGC 并没有证明 P ≠ NP；特定图仍可能得到更好的解，仅凭 P ≠ NP 也不能把该排除结论扩展到随机算法。

---

AI 怎样从开放问题中产生这些研究结果？

OpenAI 在模型开发中用尚未解决的数学研究问题进行评测。已有数学评测的成绩趋于饱和后，团队扩大了这类研究问题评测：如果原来的题目越来越难区分模型能力，就需要更难、更开放的问题。部分新输出还建立在模型先前得到的成果之上。

随后，他们在 官方发布文章 中宣布公开这一批成果，并在 GitHub 成果库 中公开了以下材料：

1. 约 4,000 个问题的尝试：在评测过程中，研发团队向该模型提出了大约 4,000 个数学研究问题。模型给出解答后，团队按照重要性标准进行聚合，最终筛选整理出 372 个成果家族（Families），共计 722 篇论文手稿（Manuscripts）。
2. 算力消耗的等价口径：据 OpenAI 的估算，平均每个成果消耗的算力，约为 使用该内部模型进行 3 小时 ChatGPT Pro 思考的等价计算量。这是算力估算口径，不是逐题实际耗时或付费金额，也不表示公开版 ChatGPT Pro 已具备同样的能力。
3. 推理过程与证明文件：官方还公开了 10 份代表性成果的推理过程摘要（经过精简的探索与推导记录，并非完整原始运行日志），以及一部分基于 Lean 语言的形式化代码。

722 篇手稿和 372 个家族使用的是不同计数单位。在这个成果库里，一个“家族”是围绕同一个核心议题组织起来的一组论文。它可能包含一篇主攻核心猜想的主论文、几篇推导衍生结论的副论文、不同推导路线的备选证明，或者是对技术细节的补充论证。因此，手稿篇数不是独立解决的问题数；再加上结果经过聚合与重要性筛选，也无法用 372 或 722 除以 4,000，算出可靠的解题成功率。

仓库说明 明确指出，尚未形式化的结果可能有问题，并承诺尽快修正。大多数结果采用同一流程，但 ζ 函数无零点区域与复乘阿贝尔簇霍奇猜想的工作属于例外；其中 11/12 无零点区域的稿件由人类编辑过，以改善可读性。

成果总览 中的 372 个家族覆盖了 17 个数学学科。其中分布较多的方向包括理论计算机科学（40 个家族）与组合数学（37 个家族），此外也涵盖代数、数论、微分几何等众多领域，体现出横跨多个数学方向的评测广度。

推理过程摘要的价值：展现自检与修正，而非正确性保证

除了最终的论文与形式化代码，官方公开的 10 份推理过程摘要提供了观察模型推导过程的窗口。这些摘要记录的并不是一帆风顺的直接证明，而是展示了包含假设失败、发现冲突后的自检修正，以及对既有数学定理依赖的探索轨迹。

例如，在圆周率无理数指数的探索记录（家族 017 摘要）中，模型曾尝试一种与罗斯（Roth）定理有关的多变量方案，但拿已知的刘维尔数一检验，发现该论证会导致“所有数的逼近指数都是 2”这一与已知反例相悖的荒谬结论，从而发现推理泛化过度，回查缺失的条件；在相对论弗拉索夫-麦克斯韦系统的记录（家族 362 摘要）中，模型多次发现粒子速度控制在长区间内失效，进而反复修正区间缩短因子，并细致检查了引用经典延拓定理所需的正则性条件，但整个论证最终仍须由模型自己证明关键的角向占据与动量估计。这些记录展现了包含失败、自检、修正和文献依赖的探索过程；它们是经过精简的推导摘要，不是已经过独立检验的正确性证书，更不能以此夸大所有推理摘要的完备性或模型的整体成功率。

---

这些突破，目前能核查到哪一步？

这批手稿中有不少附有 Lean 形式化证明。它提供了一条让计算机检查逻辑推导的路径。

什么是 Lean 形式化？

传统数学论文主要采用自然语言夹杂公式叙述，往往包含依赖数学直觉的论证步骤。而交互式定理证明语言 Lean 则要求将数学定义、定理陈述和每一步推理，严格翻译成计算机形式系统能够逐项检查的类型与代码。当证明脚本能够被逻辑内核完整编译、且未调用任何允许列表之外的公理时，即可确认整条推导链条在形式系统内部是闭合自洽的。

不过，形式化验证的确定性有其明确的边界。机器内核只负责审查给定的推导步骤是否符合形式规则，并不会自动评估这个形式化陈述是否真正忠实于论文原稿或数学界最初关注的核心难题，更不会评估该成果在数学上是否具有原创贡献，也无法解释证明背后的数学思想为何能够奏效。

自动裁判 Comparator 的核对逻辑

为了对批量生成的 Lean 证明开展自动化裁决，社区设计了裁判工具 Comparator。它并不是对代码进行表面文本的逐字比对，而是在受控环境中通过导出语法环境，严格比对提交的解答（Solution）是否准确证明了出题文件（Challenge）所指定的同一数学命题。

要让这套自动化判决真正可信，必须依赖几项核心前提：出题文件及其依赖环境完全受控可信、编译前未被外部不可信文件污染、运行沙箱工作正常，以及至少有一个底层逻辑内核是完全正确的。

“定义漏洞”的特定风险与人工复审

在形式化评测中存在一种被称为“定义漏洞”（Definition Holes）的特殊情形。这并不是指所有形式化证明都存在作弊空间，而是特指某些允许解题者自行填补定义的特定挑战。

例如，在某些需要判定猜想真假的题目中，如果挑战本身包含未定值的命题变量，提交者可能直接把该变量在解答中定义为“原猜想本身”，从而仅通过逻辑自反性轻松通过机器编译。这种做法实际上绕过了给出真实真假判定的测试意图。因此，Comparator 技术文档明确指出，凡是包含定义挖空的挑战，都必须由人工或其他额外核查来确认定义是否满足原来的任务意图。这是针对这类挑战的检查要求。

---

这些结果怎样进入数学界的共同研究？

位于普林斯顿的 高等研究院数学与人工智能顾问组（AGMAI），在收到 600 多份数学界反馈后，公开了一份 应对规范建议。OpenAI 咨询过该组，并参考了其建议；顾问组在建议中表达了自己的批评立场。

得到答案之后，人类仍要能讲清证明

顾问组反对在科学界无法访问的专有模型上测试高级数学问题，并要求实验室停止这种做法。它同时给出了在这一现实情境下发布成果的建议。 数学研究既要得到答案，也要形成 人能解释、别人能理解和继续使用的思想。传统的学术规范是：论文作者必须自己真正理解证明的每一个环节，自己对正确性负全责，并在学术研讨会上向同行公开演讲、答疑解惑。

为此，顾问组根据人类对论证的理解程度明确划分了两条处理路径：对于已有数学家充分理解论证细节并愿意对内容负全责的成果，应当沿用学术共同体的传统规范，由相关数学家发布预印本、提交学术期刊同行评审，并在学术讲座与会议上报告交流；只有当 AI 产生的数学论证尚未被提示它的研究者充分理解、无人能即时负责时，才适用专门制定的发布规范与配套资助建议。对尚未消化的输出，公开文件只是起点，还需要支持数学家理解和继续研究。

让结果进入共同研究，需要哪些工作？

对尚无人充分理解的 AI 数学输出，顾问组提出了以下建议：

1. 补文献归属，改善可读性：AI 实验室应检索相关文献、补上相关的历史先驱引用；必须把模型输出的那些充斥着怪异行话、冗长啰嗦的草稿，重写成传统数学界看得懂的友好论文，清楚交代问题、定理和证明。
2. 保存可引用、可追溯的版本：成果必须及时存入独立于商业公司的公共学术仓储（具备持久引用标识、修改记录，最好也允许同行评论），顾问组强烈建议避免把数学结果的发布当作模型营销。
3. 公布尝试情况与实验细节：实验室应公开模型名称、所用提示词、思维链摘要、算力消耗，还应说明 在多少同等难度的题目上失败了，以及题目究竟是怎么挑出来的。
4. 尽可能形式化：尽量提供符合标准的 Lean 代码与裁判比对工件，尚未形式化或依赖哪些标准结果，应清楚说明。
5. 资助人类理解，由独立机构分配支持：AI 公司有责任出资设立专项研讨会、工作组、博士后岗位和专著撰写基金，帮助人类理解这些知识；支持的分配应交给独立的非营利机构，理解工作由学术社区主导，接受资助也不意味着认可实验室的做法。
6. 让全球数学界公平访问研究工具：专有模型可能造成实验室与学术界的分层，经济条件不同又可能扩大访问差距。顾问组强烈建议向全球数学界公平、广泛地开放模型能力，使验证、共同理解与后续研究能够广泛展开。

---

AI 正在为开放的数学问题提供怎样的研究材料？

这六个例子呈现出数学研究的不同推进方式：给猜想寻找证明，用反例否定猜想，确定算法在最坏情况下的能力界限，并把已有结果用于新的问题。团队在既有数学评测趋于饱和后，转向尚未解决的研究问题；这批手稿让人们能具体观察，AI 怎样参与这些没有现成标准答案的探索。

OpenAI 集中公开的 722 篇论文手稿、部分命题的 Lean 形式化代码、10 份代表性推理摘要、约 4,000 道题目的筛选统计以及保留历史修改的版本机制，为观察这种转变提供了具体样本，也为数学界进行逐项复查与针对性检验准备了原始物料。

把成果变成可继续使用的知识，需要弄清构造为什么有效、依赖哪些条件，以及哪些思路来自已有文献。第 5 例提供了具体示范：理解 ab = 1 怎样保证输入不被混淆，以及 ba ≠ 1 怎样产生无法到达的输出，才知道如何把代数构造用于细胞自动机；想更换对象或条件，也需要回到这两步检查哪里仍然成立。Lean 可以核对形式推导，人类理解则让关键方法能被解释、修改和迁移，这正是顾问组要求支持的工作。同时，“公开研究成果”与“开放研究工具”仍是两件事：生成论文的内部模型尚未公开，数学家还不能直接复用同样的工具去重现推理或探索其他课题。

针对学术界的关切，OpenAI 提出了一系列正在推进的计划，包括探索由学术社区托管的仓储方案、在后续版本中继续完善先驱文献引用与可读性阐释、资助相关学术研讨会以协助理解重点成果，并表示正在负责任地推进该模型的公开发布。从公开的候选成果，到真正成为可检查、可解释、可接续的可靠数学知识，这批手稿仍需经历学术共同体严谨而长期的消化与检验。