722 篇手稿一夜发布：拆解 OpenAI 数学工厂的四大技术支柱

722 篇手稿一夜发布：拆解 OpenAI 数学工厂的四大技术支柱

【免费下载链接】math项目地址: https://gitcode.com/gh_mirrors/math58/math

2026 年 10 月，OpenAI 一次性公开了近 722 篇由内部模型产出的数学手稿，覆盖 372 个结果家族——从准黎曼猜想（quasi-Riemann hypothesis）的零点半平面、Catalan 常数的无理性，到 CM 阿贝尔簇上的有理 Hodge 猜想与希尔伯特第十问题在 ℚ 上的否定解答。中文社区用"数学大爆炸""数学的广岛时刻"来形容这次发布，而英文媒体则更多聚焦于一个关键细节：其中一部分手稿可以被计算机逐行验证。这份仓库（math）既是结果集，也是一条完整"AI 数学研究流水线"的活体标本。本文基于仓库源码，拆解支撑这次发布得以成立的四大技术支柱。

722 与 719：一次罕见的"模型产出"学术发布

先澄清一个数字。新闻标题里的 722 与仓库当前目录中的 719 之间的差异，本身就是这个故事的一部分。仓库根目录的 README.md 明确写着：

The current catalogue contains 719 manuscripts organized into 372 families.

而 history.md 的更新记录显示，在发布次日（October 7, 2026）的维护中，团队因一个符号错误（sign error）导致"稳定化-迹相消论证"失效，撤回了三篇相互依赖的手稿：

• Algebraicity of Weil classes on split abelian eightfolds
• Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
• The rational Hodge conjecture for products of K3 surfaces

同时修订了 14 篇存在证明修补、陈述修正、假设澄清问题的手稿，并新增 6 个形式化证明。也就是说：发布口径是 722，撤回 3 篇后仓库以 719 篇、372 个家族的状态对外呈现。撤回机制、修订记录、旧版本留存——这套版本纪律是仓库 README 中明确承诺的发布策略，也是它区别于普通 preprint 服务器之处。

从 CONTENTS.md 的手稿地图可以看出覆盖面的广度：Milne 有理猜想与代数特殊化、椭圆曲线的完整 BSD 公式、Dirichlet L 函数在 Re s > 7/8 的无零点半平面、Goldfeld 猜想、π 的无理性指数等于 2、Margulis–Platonov 猜想、限制性几何 Langlands 等价……数论、代数几何、Langlands 纲领、双曲几何、统计物理、概率论与组合学均有涉及。这不是一次"刷榜"式的基准测试提交，而是一份按数学学科分类整理的、面向同行评审生态的成果清单。

支柱一：命题工程——从 4000 道开放问题到 372 个结果家族

整条流水线的起点不是"写证明"，而是"出题"。README 的 "How the results were produced" 一节给出了这次发布的生产参数：

The vast majority of results were obtained with the same procedure using an unreleased internal OpenAI model. On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems.

几个值得细读的工程决策：

评估饱和驱动选题扩展。官方说明指出，这些手稿来自模型开发过程中的能力评估——"We expanded these evaluations after performance on our existing mathematical evaluations saturated"。即：当既有数学基准被模型"做穿"之后，评估体系转向真实开放研究问题。这解释了为什么选题跨越如此多的深水区猜想：基准饱和倒逼评估集上探到人类研究前沿。

家族化聚合。372 个家族（family）不是 719 篇论文的简单分组。README 定义得很清楚：一个家族聚合相关论文，可能包含主结果（principal result）、伴随论证（companion arguments）、推论（consequences）或替代证明（alternative proofs）。也就是说，模型产出的不是孤立论文，而是一簇围绕同一主定理的论证网络——这符合真实数学研究中"一个结果通常需要多个技术部件"的形态。

推理摘要（reasoning traces）。除了成稿，仓库还释放了 10 份经过压缩的模型推理过程摘要，覆盖 π 的无理性指数、对称与一般 Mahler 猜想、自由群因子同构、三维相对论 Vlasov–Maxwell 系统等结果（见 README.md 的表格）。这是对"黑盒证明"的一种补偿性透明度：读者至少能看到模型的论证骨架，而不只是结论。

明确标注例外。流水线并非一成不变。README 特别说明：Riemann zeta 函数的无零点区域工作、CM 阿贝尔簇的 Hodge 猜想证明不在此固定流程内；而 Re(s) > 11/12 无零点区域的手稿经过了人工可读性编辑。这种"哪些按流水线生产、哪些是例外"的边界说明，是理解这份仓库可信度的重要上下文。

支柱二：Lean 形式化验证——约 42% 顶层结果的机器背书

如果说命题与推理构成了"产出端"，那么 Lean 形式化体系就是这条流水线的"质检闸门"。仓库中lean/目录包含 3,619 个.lean文件，按数学学科组织——OAI/Algebra、OAI/Analysis、OAI/Geometry、OAI/NumberTheory、OAI/Probability、OAI/Computability等。单一入口 lean/OAI.lean 通过 900 余行import语句把整个形式化库串联起来，从 AffineCancellation（仿射消去）到 PrescribedRicci（预定 Ricci 曲率），再到 Zeta 函数的非零性证明。

README 给出的覆盖率是：~42% 的顶层结果已被形式化（300/719）。这个数字本身就是一个诚实的声明——它不是"全部可验证"，而是"将近一半"。

关键机制是Comparator 挑战验证。lean/ComparatorChallenges/README.md 描述了完整的核验工作流：

lake update lake exe cache get lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

每个挑战由一个 JSON 配置驱动。以准黎曼猜想为例，QuasiRiemannHypothesis.json 的内容如下：

{ "challenge_module": "ComparatorChallenges.QuasiRiemannHypothesis", "solution_module": "OAI.NumberTheory.DirichletL.Nonvanishing", "theorem_names": [ "OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re" ], "definition_names": [], "permitted_axioms": [ "propext", "Quot.sound", "Classical.choice" ], "enable_nanoda": false }

这份配置的语义值得拆解：

• challenge_module / solution_module 分离：挑战文件 QuasiRiemannHypothesis.lean 声明目标定理并留下sorry占位，而真正的证明位于解模块OAI.NumberTheory.DirichletL.Nonvanishing。Comparator 负责把两者对接，逐行核验解模块确实证明了挑战所声明的定理。
• permitted_axioms 白名单：只允许propext（命题外延性）、Quot.sound（商类型）与Classical.choice（选择公理）三个 Lean 基础公理。任何额外公理（例如sorryAx、未声明的axiom）都会导致验证失败——这正是"机器可核验"的严格性来源：证明只能建立在 Mathlib 与这些白名单公理之上。
• 定理级而非文件级验证：theorem_names 精确到单个定理名，例如OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re，对应 CONTENTS.md 中 003 号结果——"每个 Dirichlet L 函数（含 ζ(s)）在 Re s > 7/8 无零点"。

再以素数间隔结果为例。PrimeGaps.lean 把"大素数间隔的正下密度"形式化为一个可判定的有限集构造：largeGapIndices C N用Finset.filter收集满足C * log(p_n) < p_{n+1} - p_n的指标 n，主定理large_gaps_and_ratio_density断言对任意 C > 0 存在正比例 c，以及p_n/n递增指标集具有正下渐近密度——这正是 CONTENTS.md 中 026 号结果（Erdős 与 Prachar 问题的解答）。

从 GroundState.lean 可以看到形式化的真实写法：分部积分、紧支撑测试函数、拉普拉斯算子与梯度范数的恒等式，全部落在 Lean 的积分与偏微分算子基础设施上。这不是"把定理抄进 Lean"，而是把分析论证完整翻译成可机器检查的推理链。对一个由大模型产出的结果而言，这种翻译本身就是最严格的审稿。

支柱三：版本治理与撤回——自动化定理证明的现状与边界

第三根支柱往往被标题党忽略，但它恰恰决定了这份仓库的专业成色：对自身局限性的显式管理。

未形式化部分的风险声明。README 直言不讳：

Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly.

约 58% 的结果没有 Lean 形式化伴随，它们的正确性只能依赖传统阅读审查。这个声明把"机器已验证"与"仅人工阅读"两个层次明确区分开来，而不是把所有 719 篇笼统地宣传为"AI 证明"。

撤回与修订是机制而非事故。history.md 的 October 7, 2026 条目展示了完整的治理动作：撤回 3 篇（含依赖连锁）、修订 14 篇（含证明修补、语句修正、过时引用更正）、更新 13 篇的引用版本，并补充 6 个新形式化。README 承诺 "Corrections and revisions will be recorded as new versions, with previously released versions remaining accessible"——旧版本可访问、新版本可追溯。这种"发布后仍可撤回、撤回有解释"的做法，是 preprint 生态健康运转的必备纪律，也是大模型产出内容进入严肃学术圈的前提。

44% 之外的结构性边界。即使是被形式化的那部分，也存在类型学上的局限。ComparatorChallenges 的 README 明确区分"支持性结果验证"与"主定理验证"：像CharacterVarietiesAllSeamsSupport.json、CartierChartCompactnessSupport.json这类挑战，验证的是主定理证明中使用的关键支撑引理（如 seam 方程的相容性、chart 场收缩的紧性），而非论文最终定理本身。README 还提到正在探索社区托管仓库（community-hosted repositories）作为这些材料的补充分发渠道。这些细节共同勾勒出"大规模自动定理证明"的当前边界：机器可以逐行核验论证，但"论证的组织、意义的筛选、结果的归属"仍需要人在回路中。

支柱四：可复现的产出管线——一条可以被研究、被模仿、被质疑的流水线

把前三根支柱串起来，第四根支柱浮出水面：整条管线是可复现的、可审计的、可再生产的。

从命题（4000 道开放问题）→ 推理（平均 3 小时 thinking compute）→ 聚合（372 个家族）→ 形式化（42% 顶层结果）→ 治理（撤回/修订/版本化），每个环节在仓库中都有对应的人工产物：README.md 描述流程，CONTENTS.md 提供按结果家族索引的手稿地图，lean/提供机器核验层，history.md 提供审计轨迹。这意味着任何研究者都可以：

• 挑出 CONTENTS.md 中感兴趣的家族，阅读手稿；
• 对带[Lean]标记的结果（如 003、005、007、012、013、017、020、021、023、024、025、026、027、028、033 等，见 CONTENTS.md），用 Comparator 在自己的机器上重新跑一遍形式化验证；
• 对照 reasoning traces 检查模型的论证骨架；
• 甚至以这套挑战-解模块结构为模板，把新的结果接入验证体系。

对中文读者而言，这份仓库还有一个微妙的对照价值：过去两年国产模型在 MATH、AIME 等基准上反复与 OpenAI 对线的同时（Kimi k0-math、DeepSeek R1、通义 QwQ 都曾在中文社区以"超越 o1"为卖点），OpenAI 选择了另一条路——不刷基准，而是把模型扔进数学研究的深水区，并把手稿、验证、治理一并开源。基准测试检验的是"解题能力"，这份仓库检验的是"研究能力"，而后者显然更难被榜单量化。

结语：数学研究会被流水线化吗

722 篇手稿的发布（现为 719 篇）真正冲击数学界的，不是"AI 会做难题"——这个信号早已出现——而是研究过程的工业化形态：命题可以批量构造，推理可以按小时计费地规模化，验证可以由机器逐行完成，治理可以像软件发布一样打版本、撤回、修订。准黎曼猜想、Catalan 常数无理性、希尔伯特第十问题在 ℚ 上的解答，这些名字足以吸引眼球，但仓库真正值得反复阅读的，是 README 中那句克制的话："As part of model development, we evaluate our models on open research problems."——数学前沿从此成为模型开发的质量标尺，而这份仓库，就是那把标尺第一次被完整地公开校准。

【免费下载链接】math项目地址: https://gitcode.com/gh_mirrors/math58/math