OpenAI 10 月 6 日发布的数学成果，为公众提供了一个包含 722 篇手稿、按 372 个结果系列组织的合集。一个系列可以包含多篇论文，而形式化证明的范围可能比关联手稿中的论断更窄。从仓库中的论文追踪到其证明配置，可以看出具体选择了哪项论断进行检查。

BIG CHANGE 于 10 月 7 日检查了仓库的完整文件清单、目录和选定的证明工件。这是文档审阅和静态工件分析；我们没有编译 Lean 库、运行证明检查器，也没有评审数学内容。OpenAI 的公告将此次发布描述为持续演进的版本，并称后续还会增加形式化内容。

重大变化

  • 有哪些变化：研究人员现在可以通过共享的公开目录，追踪数百篇 AI 生成手稿及其支持文件；部分结果还附有形式化陈述和拟议的证明实现。
  • 为何重要：数学家在考虑是否使用某项结果时，可以查看实际选中进行检查的陈述、它的假设，以及它与论文的关系。仓库的组织方式有助于识别较窄的形式化结果止于何处，以及进一步数学审查从何处开始。
  • 后续值得关注：OpenAI 计划增加形式化内容并保留修订记录。这些更新关系到引用或依赖相关工作的读者：审查记录需要指出所检查的版本和定理。

分别统计手稿与系列

我们的清单在 preprints/ 下发现 722 个直接存放手稿的目录，每个目录都含有 PDF；在 reasoning_traces/ 下还发现 10 个 PDF。手稿地图包含 372 个不同系列条目，并链接到 722 篇手稿。

这些数量代表不同对象：

工件

读者可以查看的内容

结果系列

相关论文的分组，可包括配套论证、推论或替代证明。

手稿

一份独立的数学文档，拥有自己的源文件和引用信息。

推理摘要

模型针对某项选定结果给出的推理简述。

Lean 工件

形式化定义、陈述和拟议证明，并提供链接和配置来说明待检查内容。

仓库的 README解释了这些类别，并提醒读者各项内容的验证程度并不一致。有些结果没有 Lean 形式化；OpenAI 也表示，未形式化的工作可能存在问题。形式化目录本身将适用范围记录为“部分进展”，审查状态为 unchecked。这些字段是发布元数据，并非 BIG CHANGE 运行检查器所得的结果。

无需 OpenAI 账户即可阅读这些公开文件。公告称，生成模型目前为内部模型，OpenAI 正在努力发布它。因此，能够访问这些文档并不代表能够访问该模型。

追踪证明前先固定版本

本文使用的仓库快照对应提交 adc7f1241b42e322a6451854ab7e4b4c146bf78a，日期为 2026 年 10 月 6 日 21:58:50 UTC。包含此标识符的链接会固定到本文检查的快照；包含 main 的链接则指向不断变化的默认分支。OpenAI 的 README 承诺在出现更正或修订时保留早期版本。

先查看 概览，按数学主题对系列分组，再通过手稿地图找到具体论文。记录其目录名、仓库提交和论文所附引用。手稿日期可能与合集发布日期不同。

系列 003 包含一篇论文，主张在 7/8 右侧存在无零区域；另一篇给出 11/12 右侧区域的替代证明；还有一篇单独讨论 Landau–Siegel 零点。第一篇论文的目录标注日期为 9 月 30 日，并提供 BibTeX 引用。记录具体论文有助于区分这些主张。

其 Lean 范围页面说明形式化内容覆盖哪些陈述、列出排除项，并指出论文中的后续应用未被纳入。页面链接到针对 zeta 结果、Dirichlet 与 Hecke L 函数以及统一实零点间隔的独立检查陈述。检查其中一个选定陈述，不会自动代表该页面上的所有项目。

沿着选定陈述查看其配置

OpenAI 的 Comparator 说明以系列 003 为例。Comparator 用于比较拟议的 Lean 证明与指定挑战。示例中的 JSON 配置选择了一项定理：当黎曼 ζ 函数自变量的实部大于 7/8 时，该函数不为零。

配置指向一个挑战模块和一个独立的解答模块。它允许使用标准公理 propext、Quot.sound和 Classical.choice，并将 enable_nanoda设为 false。Nanoda 是 Comparator 可调用的独立检查器；此处提供的配置并未启用它。

挑战文件包含 ，这是 Lean 对未完成证明的占位符。在此处，它提供要匹配的陈述。Comparator 文档允许挑战中出现占位符，但要求解答中提供正确证明。仅在这个挑战中发现 sorry，不能说明独立解答是否通过。sorryComparator 文档。若要按文档进行本地检查，输入包括该配置、挑战与解答模块及其依赖项。仓库固定使用

Lean 4.34.1。其 Lake 清单记录依赖项版本，包括 Mathlib 的 。OpenAI 要求将 d13f23b723b8a846827a245b89c10fc7d3f11612、

和 comparator加入可执行文件搜索路径，然后从 landrun 目录运行以下命令：lean4export这些是发布者的说明，不是我们实际运行过的命令。它们没有固定这三个外部工具的版本。Comparator 的当前文档要求使用兼容版本的 lean/，说明其沙箱前提，并列出成功结果能够证明与挑战匹配、使用获准公理以及通过内核接受的条件。可复现报告还需要记录已安装工具版本和实际输出，以及仓库提交。

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

Lean 库的 lean4exportREADME

建议编译这个大型库中的小部分内容。它还记录了 Linux 内存映射限制，这些限制可能阻止完整构建。我们没有测量此示例的本地运行时间或硬件成本。按其声明范围理解成功检查Lean 的

验证参考文档

在查阅时为 4.35.0-rc3 版本，它区分了形式证明被接受与理解定理含义。这一文档版本不同于该仓库固定的工具链版本。基本检查成功，意味着内核依据相应定义、导入和公理接受了形式陈述。依赖项仍可能包含未完成的证明。Lean 文档介绍了 ，用于显示所用公理；其中包括依赖链中未完成证明所用的

。#print axioms更严格的检查会重放已存储的证明，或将解答与单独指定的陈述进行比较。但它们仍取决于检查环境，以及形式表达是否正确体现了预期含义。因此，验证报告应记录具体挑战、获准公理和外部检查器设置。内核接受或与挑战匹配，都不能证明期刊已接收论文，也不能证明手稿中的每项主张都已形式化。sorryAx计算量数据描述的是生成过程

OpenAI 报告称，每项结果平均使用了相当于约三小时 ChatGPT Pro 思考的计算量。其 README 说，评估提出了约 4,000 道题，随后对输出进行分组并挑选重要结果。README 也列出了通常流程的例外。这些是公司的生成数据；它们不代表读者运行 Lean 检查的价格，也不是以美元计的总账单。

发布公告

、生成过程说明。对于系列 003，此次检查识别出一项具体的 zeta 陈述、拟议解答以及检查器允许的公理。它也确认所提供的示例没有启用 Nanoda。该配置检查能否成功，仍需通过实际运行并记录结果来回答。来源与延伸阅读

OpenAI 10 月 6 日的公告

说明发布日期、模型的内部状态、计划增加的内容及公司报告的计算量估算。这是开发者对自身工作的说明。