OpenAI 公开内部前沿模型的数学成果：约 4000 道开放问题筛出 722 篇稿件，含 Hodge 猜想特例与 ζ 函数零点区域，约 162 篇主结果附 Lean 证明

这件事意味着什么

【要点】

OpenAI 在 2026 年 10 月 6 日发布《Sharing AI progress in mathematics》，公开一个尚未对外发布的内部前沿模型在数学开放问题上产出的一批新结果，论文和证明材料都放进了 GitHub 仓库 openai/math。

仓库说明写道，目前收录 722 篇稿件，归为 372 个结果族，按数学分支分类。评测期间共向模型提出约 4000 个问题，按显著性筛选、合并后形成这份目录。绝大多数结果用同一套固定流程产出，平均每个结果花费相当于约 3 小时 ChatGPT Pro 思考的算力。OpenAI 说，之所以改拿开放问题来测，是因为模型在现有数学评测上的成绩已经饱和。

仓库还附了 10 份模型推理过程的摘要，题目包括 π 的无理性指数、对称 Mahler 猜想、Kaplansky 直接有限性猜想在特征 2 下的反例、自由群因子同构、三维相对论 Vlasov–Maxwell 方程组等。两项最引人注目的工作被明确列为固定流程之外的例外：黎曼 ζ 函数的零点无关区域，以及 CM 阿贝尔簇上的 Hodge 猜想证明；其中 Re(s) > 11/12 零点区域那篇的文稿经过人工润色。

部分证明用 Lean（一种让计算机逐步检查证明的语言）做了形式化。按仓库的形式化目录，目前约 162 篇稿件的主结果有对应的 Lean 证明，OpenAI 表示会陆续补充。发布方式参考了普林斯顿高等研究院数学与人工智能独立顾问组的建议，修订和引用都保留版本记录。OpenAI 还表示将资助围绕 AI 重大数学成果的研讨会和专项项目，并在推进对外发布产出这些结果的模型。

【可核验】

一手页面：https://openai.com/index/sharing-ai-progress-in-mathematics

成果仓库：https://github.com/openai/math （README、overview.pdf、CONTENTS.md 和 lean/formalization.yaml）

OpenAI RSS 标注的发布时间是 10 月 6 日 12:00（GMT）。稿件数、问题数和算力估计都来自 OpenAI 自己的仓库说明，README 里也直说「部分未形式化的结果可能有问题」。形式化目录本身的人工审查状态标为 unchecked，也就是说，Lean 能检查证明是否成立，但形式化的命题是否忠实对应论文里的说法，还没有人逐一核对。Hodge 猜想那项不在形式化目录里。截至发稿，数学界还没有对头部结果给出公开的独立复核结论。

【我们的判断】

这次真正值得注意的不是某一道题，而是数学成果的产出方式变了。约 4000 道题、平均每道 3 小时算力、最后筛出 722 篇稿件，说明前沿模型已经可以当成一条持续运转的研究流水线来用，而不只是偶尔出彩的解题助手。OpenAI 自己承认现有数学评测已经饱和，这本身就是一个能力信号。

瓶颈随之转到了验证这一边。722 篇稿件远超任何审稿体系一次能消化的量，有 Lean 证明的不到四分之一，而且形式化命题与原文是否一致还没人审。最轰动的 Hodge 猜想特例和 ζ 零点区域恰好是流程外的例外，最需要谨慎看待。接下来值得盯三件事：数学家对头部结果的独立复核，Lean 覆盖率和命题审查能推进多少，以及产出这些结果的模型何时、以什么形式开放。在这些落地之前，把它读成「AI 已经证明了 Hodge 猜想」是过度解读；读成「科研产出不再稀缺，验证能力成了新瓶颈」更接近事实。