新聞｜OpenAI 公開內部模型的 722 篇數學稿件，含準黎曼假設的證明宣稱

重點

OpenAI 10 月 6 日（美國時間）在 GitHub 儲存庫 openai/math 公開 722 篇數學稿件，分成 372 個結果家族，全部出自一個尚未釋出的內部模型，橫跨 17 個數學領域。
官方說模型在評估中被問了約 4,000 個開放問題，平均每個結果花掉約相當於 ChatGPT Pro 三小時的思考算力。
最受注目的是準黎曼假設：所有 Dirichlet L 函數（含 Riemann ζ 函數）在 Re s > 7/8 沒有零點。這個結果附有 Lean 證明，已有獨立團隊用兩個 kernel 重跑通過，但它沒有走 OpenAI 的固定產出流程。
形式化目錄列出 162 篇稿件的主結果有 Lean 證明，約占 22%；日期在 10 月 3 日到 6 日的 143 篇稿件全都沒有。
數學界的批評集中在一次大量釋出、模型與提示詞不公開、沒有同儕審查，以及搶走研究者正在做的題目。

發生了什麼

OpenAI 在部落格文章〈Sharing AI progress in mathematics〉宣布釋出這批結果，同時開放儲存庫 openai/math（Apache-2.0 授權）。儲存庫的第一個 commit 在太平洋時間 10 月 6 日下午 2 點 58 分，台灣時間 10 月 7 日清晨。

儲存庫的內容：

preprints/：722 份稿件的 PDF、原始檔與 BibTeX
overview.pdf：372 個家族的摘要目錄
lean/：Lean 4 形式化程式庫、形式化目錄 formalization.yaml 與 Comparator 檢查設定
reasoning_traces/：10 個結果的模型推理摘要（節錄版）

一個家族把相關稿件歸在一起，可能包含主結果、配套論證、推論或替代證明。所有稿件的作者都署名 OpenAI。官方承諾修訂會以新版本記錄，舊版保留可查。

怎麼產出的

README 說，OpenAI 原本用數學評測集測試模型，這些評測飽和之後，才改成直接拿開放研究問題來測。流程是：

評估期間對模型提出約 4,000 個問題
絕大多數結果用同一個固定流程得到，平均每個結果約等於 ChatGPT Pro 三小時的思考算力
把輸出整理成家族與稿件，再用一個「足夠重要」的門檻篩選，最後留下 372 個家族

有些結果建立在模型更早產出的結果上。README 列出兩個例外：ζ 函數的零點自由區域，以及 CM 阿貝爾簇的 Hodge 猜想，兩者都沒有走固定流程。Re s > 11/12 那篇的寫法也經過人工編輯。

OpenAI 發言人告訴 Scientific American，幾乎每個結果都來自交給單一 agent 的單一提示詞，但也承認有些結果可能試了不只一次。上個月的 Navier–Stokes 證明動用了約一萬個 agent，算力成本達數百萬美元。

各領域的家族數：

領域	家族數
理論計算機科學	40
組合學	37
代數與複幾何	36
數論	31
機率與統計力學	29
微分幾何	29
數學物理	25
其他 10 個領域	145

準黎曼假設

黎曼假設說，ζ 函數的非平凡零點都落在 Re s = 1/2 這條線上。準黎曼假設弱一些：只要求存在某個小於 1 的常數 θ，使 ζ 在 Re s > θ 的整個半平面上沒有零點。過去一百多年已知的零點自由區域都貼著 Re s = 1，而且越往虛軸高處越窄，從來沒有一條固定寬度的帶狀區域。

家族 003 的主稿件是 199 頁的〈The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re s > 7/8〉，日期為 9 月 30 日。它宣稱：

所有 Dirichlet L 函數在 Re s > 7/8 沒有零點，ζ 也包括在內（s = 1 的極點除外）
同樣的半平面對 Q(√−3) 上所有有限階 Hecke L 函數成立
證明先處理 Q(√−3) 的 Hecke 家族，再轉移到 Dirichlet 的情形

同一家族還有兩篇：

10 月 5 日，49 頁：用不同方法證明較弱的 Re s > 11/12，註明「在人類協助下寫成」
10 月 1 日，9 頁：一致排除 Landau–Siegel 零點，也就是存在絕對常數 c > 0，使每個實原始非主特徵的 L 函數，其實零點 β 都滿足 (1 − β) log q ≥ c

Comparator 檢查的 ζ 敘述只有一行：對 Re s > 7/8 的複數 s，Mathlib 定義的 riemannZeta s ≠ 0，只允許 propext、Quot.sound、Classical.choice 三個標準公理。Dirichlet 與 Hecke 的版本各有一個敘述。範圍說明寫出了沒有涵蓋的部分：

論文後段的應用沒有形式化
Siegel 零點的結果沒有給出 c 的具體值，只排除 1 − c/log q < β < 1 這一段，(0, 1) 其他位置的實零點不在範圍內

10 月 7 日，一個獨立團隊在 GitHub 專案 davegoldblatt/openai-zeta-proof-check 重跑了 ζ 的檢查。Lean 預設 kernel 與另一個用 Rust 獨立實作的 nanoda kernel 都接受了證明，用到的公理也只有上述三個。這份證明約 2,900 個檔案、將近 50 萬行。團隊特別說明，他們只檢查了 Lean 證明，沒有審閱論文本身，而且只在一台機器上跑過。

羅格斯大學的數學家 Alex Kontorovich 在 X 上寫道，如果這是人類做到的，「會立刻拿到費爾茲獎，沒有疑問」。

其他主要宣稱

家族	宣稱	Lean 形式化
002	Selmer 餘秩 0 或 1 的有理數橢圓曲線滿足完整的 BSD 公式	未列入
017	π 的無理性指數恰為 2	有，Flint–Hills 級數的推論不在內
032	CM 阿貝爾簇的有理 Hodge 猜想	未列入，也沒有走固定流程
087	對稱與一般形式的 Mahler 猜想	有，函數形式的不等式不在內
102	Khot 的 Unique Games 猜想，以及 Max-Cut、Vertex Cover 的近似困難度	有
287	所有非交換自由群因子彼此同構	有，基本群的推論不在內

Nature 指出，這批稿件沒有解決剩下五個千禧年大獎難題中的任何一個，但有幾篇跟 Hodge 猜想、黎曼假設有關。OpenAI 發言人說，重要性「留給更廣的數學社群評估」。

Lean 涵蓋了多少

Lean 能保證的是：形式化敘述在給定的定義、匯入的定理與公理下成立。敘述是否忠實對應論文的宣稱，要靠人來核對，結果重不重要也一樣。New Scientist 指出，這批結果的 Lean 敘述跟論文對不對得上，目前還沒有人檢查。

儲存庫裡的數字：

formalization.yaml 列出 162 篇稿件有主結果的形式化，占 722 篇的 22%
Comparator 設定共 185 個，一篇稿件可以對應多個
lean/docs/ 有 235 個家族的形式化範圍說明
README 自己註明「部分未形式化的結果可能有問題」，並說會陸續補上形式化

依稿件資料夾上的日期分組：

稿件日期	稿件數	有 Lean 主結果
9 月 10–18 日	4	0
9 月 22–27 日	567	159
9 月 30 日–10 月 2 日	7	3
10 月 3–6 日	143	0

另有 1 篇沒有標日期。越接近釋出日寫成的稿件，形式化越少。

爭議

9 月 21 日，OpenAI 因為 Navier–Stokes 結果的公布方式引發爭議，宣布組成獨立的數學家諮詢小組，也就是高等研究院（IAS）的 Advisory Group on Mathematics and Artificial Intelligence。依 Scientific American 與 New Scientist 的整理，小組的建議跟這次的做法對照如下：

小組建議	這次的做法
公開模型名稱	只稱「內部前沿模型」
公開每個結果的提示詞	未公開
公開算力成本	只給平均約三小時 Pro 算力
盡可能形式化	162 篇有主結果的形式化
揭露失敗的題目與選題方式	只給出約 4,000 題的總數

OpenAI 發言人對 Scientific American 表示，公司認真看待這些指引，但不受其約束。

其他批評與回應：

WIRED 報導，OpenAI 8 月召集約 40 位數學家討論，與會者說公司當時保證不會一次釋出全部結果；發言人 Lindsay McCallum 說公司「不知道有這個保證」。
康乃狄克大學的 Alvaro Lozano-Robledo 說一次釋出的數量「驚人」，質疑為什麼要一次解幾百個問題。有研究者抱怨自己的題目被搶先，一位物理學家稱之為「slopocalypse」。
MIT 的 Andrew Sutherland 說，在模型釋出、外界能重現之前，「單一 agent 一次解出」的說法都應視為未經驗證。
多倫多大學的 Daniel Litt 認為，既然想知道這些問題的答案，沒有理由要公司保密。
Anthropic 的數學家 Levent Alpöge 說會有研究者的計畫因此落空，但仍稱這是「數學史上最重要的時刻」。
OpenAI 發言人也對 Scientific American 承認，許多新結果連公司自己的數學家都還沒弄懂。

限制與未知

模型的名稱、規模與提示詞都沒有公開，外界無法重現產出過程。
稿件都沒有經過同儕審查。
560 篇沒有形式化的稿件，正確性要靠人工審閱。
已形式化的結果，Lean 敘述與論文主張是否一致，還待人工核對。
「重要性門檻」怎麼定、約 4,000 題中哪些失敗，都沒有說明。
部分結果建立在模型更早的結果上，上游若有錯，可能牽連下游。