AI-translated from English; not yet reviewed by a fluent editor. # OpenAI 数学仓库：手稿、版本与 Lean 证明 > OpenAI 的合集包含 722 篇手稿，归入 372 个系列。仔细查看一项 Lean 证明配置，可以了解如何检查版本、适用范围和验证要求。 By BIG CHANGE Editorial Published: 2026-10-07T04:13:00.689Z Updated: 2026-10-07T04:13:00.689Z Canonical: https://bigchange.ai/blog/openai-math-repository-manuscripts-formal-proofs ![Charcoal concept illustration of one reader holding loose manuscript folios, seen from behind, beside a second stack with an orange tab.](https://bigchange.ai/api/media/file/openai-math-manuscript-reading-hero-v1.png) AI-generated conceptual illustration by BIG CHANGE. OpenAI 10 月 6 日发布的数学成果，为公众提供了一个包含 722 篇手稿、按 372 个结果系列组织的合集。一个系列可以包含多篇论文，而形式化证明的范围可能比关联手稿中的论断更窄。从仓库中的论文追踪到其证明配置，可以看出具体选择了哪项论断进行检查。 BIG CHANGE 于 10 月 7 日检查了仓库的完整文件清单、目录和选定的证明工件。这是文档审阅和静态工件分析；我们没有编译 Lean 库、运行证明检查器，也没有评审数学内容。[OpenAI 的公告](https://openai.com/index/sharing-ai-progress-in-mathematics/)将此次发布描述为持续演进的版本，并称后续还会增加形式化内容。 ## 重大变化 - **有哪些变化：**研究人员现在可以通过共享的公开目录，追踪数百篇 AI 生成手稿及其支持文件；部分结果还附有形式化陈述和拟议的证明实现。 - **为何重要：**数学家在考虑是否使用某项结果时，可以查看实际选中进行检查的陈述、它的假设，以及它与论文的关系。仓库的组织方式有助于识别较窄的形式化结果止于何处，以及进一步数学审查从何处开始。 - **后续值得关注：**OpenAI 计划增加形式化内容并保留修订记录。这些更新关系到引用或依赖相关工作的读者：审查记录需要指出所检查的版本和定理。 ## 分别统计手稿与系列 我们的清单在 `preprints/` 下发现 722 个直接存放手稿的目录，每个目录都含有 PDF；在 `reasoning_traces/` 下还发现 10 个 PDF。[手稿地图](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/CONTENTS.md)包含 372 个不同系列条目，并链接到 722 篇手稿。 这些数量代表不同对象： | 工件 | 读者可以查看的内容 | | --- | --- | | 结果系列 | 相关论文的分组，可包括配套论证、推论或替代证明。 | | 手稿 | 一份独立的数学文档，拥有自己的源文件和引用信息。 | | 推理摘要 | 模型针对某项选定结果给出的推理简述。 | | Lean 工件 | 形式化定义、陈述和拟议证明，并提供链接和配置来说明待检查内容。 | 仓库的 [README](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md)解释了这些类别，并提醒读者各项内容的验证程度并不一致。有些结果没有 Lean 形式化；OpenAI 也表示，未形式化的工作可能存在问题。[形式化目录](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/formalization.yaml)本身将适用范围记录为“部分进展”，审查状态为 `unchecked`。这些字段是发布元数据，并非 BIG CHANGE 运行检查器所得的结果。 无需 OpenAI 账户即可阅读这些公开文件。公告称，生成模型目前为内部模型，OpenAI 正在努力发布它。因此，能够访问这些文档并不代表能够访问该模型。 ## 追踪证明前先固定版本 本文使用的仓库快照对应提交 [`adc7f1241b42e322a6451854ab7e4b4c146bf78a`](https://github.com/openai/math/commit/adc7f1241b42e322a6451854ab7e4b4c146bf78a)，日期为 2026 年 10 月 6 日 21:58:50 UTC。包含此标识符的链接会固定到本文检查的快照；包含 `main` 的链接则指向不断变化的默认分支。OpenAI 的 README 承诺在出现更正或修订时保留早期版本。 先查看 [概览](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/overview.pdf)，按数学主题对系列分组，再通过手稿地图找到具体论文。记录其目录名、仓库提交和论文所附引用。手稿日期可能与合集发布日期不同。 系列 003 包含一篇论文，主张在 7/8 右侧存在无零区域；另一篇给出 11/12 右侧区域的替代证明；还有一篇单独讨论 Landau–Siegel 零点。[第一篇论文的目录](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/README.md)标注日期为 9 月 30 日，并提供 BibTeX 引用。记录具体论文有助于区分这些主张。 其 [Lean 范围页面](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md)说明形式化内容覆盖哪些陈述、列出排除项，并指出论文中的后续应用未被纳入。页面链接到针对 zeta 结果、Dirichlet 与 Hecke L 函数以及统一实零点间隔的独立检查陈述。检查其中一个选定陈述，不会自动代表该页面上的所有项目。 ## 沿着选定陈述查看其配置 OpenAI 的 [Comparator 说明](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/README.md)以系列 003 为例。Comparator 用于比较拟议的 Lean 证明与指定挑战。示例中的 [JSON 配置](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.json)选择了一项定理：当黎曼 ζ 函数自变量的实部大于 7/8 时，该函数不为零。 配置指向一个挑战模块和一个独立的解答模块。它允许使用标准公理 `propext`、`Quot.sound`和 `Classical.choice`，并将 `enable_nanoda`设为 `false`。Nanoda 是 Comparator 可调用的独立检查器；此处提供的配置并未启用它。 挑战文件[包含 ](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean)，这是 Lean 对未完成证明的占位符。在此处，它提供要匹配的陈述。Comparator 文档允许挑战中出现占位符，但要求解答中提供正确证明。仅在这个挑战中发现 `sorry`，不能说明独立解答是否通过。`sorry`Comparator 文档[。](https://github.com/leanprover/comparator#readme)若要按文档进行本地检查，输入包括该配置、挑战与解答模块及其依赖项。仓库固定使用 Lean 4.34.1[。其 ](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lean-toolchain)Lake 清单[记录依赖项版本，包括 Mathlib 的 ](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lake-manifest.json)。OpenAI 要求将 `d13f23b723b8a846827a245b89c10fc7d3f11612`、 和 `comparator`加入可执行文件搜索路径，然后从 `landrun` 目录运行以下命令：`lean4export`这些是发布者的说明，不是我们实际运行过的命令。它们没有固定这三个外部工具的版本。Comparator 的当前文档要求使用兼容版本的 `lean/`，说明其沙箱前提，并列出成功结果能够证明与挑战匹配、使用获准公理以及通过内核接受的条件。可复现报告还需要记录已安装工具版本和实际输出，以及仓库提交。 ```sh lake update lake exe cache get lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json ``` Lean 库的 `lean4export`README 建议编译这个大型库中的小部分内容。它还记录了 Linux 内存映射限制，这些限制可能阻止完整构建。我们没有测量此示例的本地运行时间或硬件成本。[按其声明范围理解成功检查](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/README.md)Lean 的 ## 验证参考文档 在查阅时为 4.35.0-rc3 版本，它区分了形式证明被接受与理解定理含义。这一文档版本不同于该仓库固定的工具链版本。[基本检查成功，意味着内核依据相应定义、导入和公理接受了形式陈述。依赖项仍可能包含未完成的证明。Lean 文档介绍了 ](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/)，用于显示所用公理；其中包括依赖链中未完成证明所用的 。`#print axioms`更严格的检查会重放已存储的证明，或将解答与单独指定的陈述进行比较。但它们仍取决于检查环境，以及形式表达是否正确体现了预期含义。因此，验证报告应记录具体挑战、获准公理和外部检查器设置。内核接受或与挑战匹配，都不能证明期刊已接收论文，也不能证明手稿中的每项主张都已形式化。`sorryAx`计算量数据描述的是生成过程 OpenAI 报告称，每项结果平均使用了相当于约三小时 ChatGPT Pro 思考的计算量。其 README 说，评估提出了约 4,000 道题，随后对输出进行分组并挑选重要结果。README 也列出了通常流程的例外。这些是公司的生成数据；它们不代表读者运行 Lean 检查的价格，也不是以美元计的总账单。 ## 发布公告 、[生成过程说明](https://openai.com/index/sharing-ai-progress-in-mathematics/)。[对于系列 003，此次检查识别出一项具体的 zeta 陈述、拟议解答以及检查器允许的公理。它也确认所提供的示例没有启用 Nanoda。该配置检查能否成功，仍需通过实际运行并记录结果来回答。](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md#how-the-results-were-produced)来源与延伸阅读 OpenAI 10 月 6 日的公告 ## 说明发布日期、模型的内部状态、计划增加的内容及公司报告的计算量估算。这是开发者对自身工作的说明。 - [固定版本的仓库](https://openai.com/index/sharing-ai-progress-in-mathematics/)提供本文检查的目录、手稿文件和证明配置。计数来自完整清单和手稿地图；选定的形式化文件仅供阅读，未被执行。我们检查了概览的 LaTeX 源文件，以了解其组织方式。 - [Lean 的 ](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a)验证参考文档 - [解释证明检查的含义和局限。我们使用 4.35.0-rc3 版本；OpenAI 项目固定 Lean 4.34.1。](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/)Comparator 的 - [文档](https://github.com/leanprover/comparator#readme)介绍挑战和解答文件、环境要求及有条件的保证。它没有报告对此合集进行验证的结果。 - [Curtis Pyke 在 Kingy.ai 对该发布的评述](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/)提供了独立的静态检查，并明确表示没有独立运行 Lean；我们不把它当作复现了证明检查。 - [BIG CHANGE 先前关于 AI 数学的报道](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes)覆盖了 5 月至 9 月的进展。本文检查新合集的工件结构和审阅流程。 ## Sources - [OpenAI 10 月 6 日的公告](https://openai.com/index/sharing-ai-progress-in-mathematics/) — 确认发布日期、模型的内部状态、计划增加的内容以及公司的计算量估算。这是开发者对自身工作的说明。 - [固定版本的 OpenAI 数学仓库](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) — 提供本文检查的目录、手稿文件和证明配置。计数来自完整清单和手稿地图；选定的形式化文件仅供阅读，未被执行。我们检查了概览的 LaTeX 源文件，以了解其组织方式。 - [Lean 验证参考文档](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) — 解释证明检查的含义和局限。我们使用 4.35.0-rc3 版本；OpenAI 项目固定 Lean 4.34.1。 - [Comparator 文档](https://github.com/leanprover/comparator#readme) — 介绍挑战和解答文件、环境要求及有条件的保证。它没有报告对此合集进行验证的结果。 - [Curtis Pyke 在 Kingy.ai 的评述](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) — 对该发布进行了独立静态检查，并明确表示没有独立运行 Lean；我们不把它当作复现了证明检查。 - [BIG CHANGE 先前关于 AI 数学的报道](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) — 涵盖 5 月至 9 月的进展。本文检查新合集的工件结构和审阅流程。