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 日的公告

說明發布日期、模型的內部状態、计划增加的內容及公司報告的计算量估算。這是開發者對自身工作的說明。