OpenAI 發布來自秘密模型的 722 份數學手稿,研究人員要求提出證據
重點速覽
- •OpenAI 發布了來自未公開內部模型的 722 份數學手稿,分為 372 個結果家族,據稱大部分透過給單一代理的單一提示詞生成。
- •722 份手稿中僅有 162 份(約 22%)目前包含經電腦驗證的 Lean 主結果,約 560 份尚未經正式驗證。
- •OpenAI 僅為 10 項結果發布了節選推理摘要且未提供提示詞,未達到高等研究院顧問小組 9 月 29 日的披露建議。
- •MIT 數學家 Andrew Sutherland 表示,在模型釋出且結果能被獨立重現之前,單次生成的說法應視為未經驗證。
- •Abhishek Saha 教授稱此次發布是數學界的重大一天,但指出準黎曼假設是唯一達到千禧年難題級別重要性的結果。

OpenAI 發布了 722 份由一個未公開的內部模型生成的數學手稿,並稱這些成果主要來自單一提示詞、單一代理的流程。這些論文被整理為 372 個相關結果家族,但數學家表示,在模型、提示詞及其他證據公開之前,這些說法無法獲得完整評估。
此次發布正值 AI 實驗室日益將數學作為前沿模型推理能力的試金石之際,也成為 AI 生成研究應如何發表、驗證與披露的早期測試。
OpenAI 一位發言人表示,幾乎所有成果都來自給單一 AI 代理的單一提示詞,不過部分結果可能經過多次嘗試。該公司表示,他們向模型提出了約 4,000 道題目,並挑選出其認為足以發表的輸出結果。
MIT 數學家 Andrew Sutherland 接受《Scientific American》採訪時表示,對單次生成的說法應謹慎看待。「除非他們釋出模型、讓人們能夠重現其結果,否則我認為任何關於用單一代理一次解決問題的說法都應視為未經驗證,」Sutherland 說。「我們應該要求拿出證據。」
722 這個數字代表的是手稿數量,而非已解決的問題數。一個結果家族可能包含一個主定理,以及配套論證、推論或替代證明。OpenAI 表示,平均每個結果使用了相當於約三小時 ChatGPT Pro 思考運算的資源。這與該公司上個月關於 Navier-Stokes 的主張截然不同,後者動用了 10,000 個協同運作的代理,運行 88 小時。
OpenAI 為其中 10 項結果發布了節選的推理摘要。然而,GitHub 儲存庫中的形式化目錄顯示,722 份手稿中目前僅有 162 份包含經電腦驗證的主結果。這約佔總數的 22%,意味著該結果已被翻譯成 Lean——一種能機械化檢查每個邏輯步驟的軟體。Lean 已成為數學領域機器驗證證明的事實標準,這也是為什麼約 560 份尚未形式化的手稿構成整批最主要的懸而未決問題。
OpenAI 表示並非所有手稿都有 Lean 形式化,並警告「部分未形式化的結果可能存在問題」。通過 Lean 驗證僅能確認證明符合 Lean 中所寫的陳述,並不能證明該陳述對應原始問題,也不能證明結果是新穎或重要的。這些問題仍需數學家的審查。
研究人員已對這些素材及其發布方式提出疑慮。Dmitry Rybin 在 X 上寫道:
I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026
Keith Adler 在 X 上寫道:
The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026
位於紐澤西州普林斯頓的高等研究院也質疑 AI 生成數學成果的影響。「如今 AI 能夠輸出數學論證,而提示它的人卻無法理解這些論證、驗證它們或為其負責,」該研究院在聲明中表示。「我們認為人類對數學的理解仍然至關重要。在這個新時代,我們如何努力建立一個將人類對數學的理解納入負責任學術成果的新典範?」
Abhishek Saha 教授則持較正面的看法,他寫道:「這是數學界非常重大的一天。」他表示大部分結果屬於「既有計畫中的卓越進展」和「令人驚訝的突破」等類別。在他的評估中,這批成果包含有趣的問題,但沒有可與千禧年大獎難題——克雷數學研究所的七道百萬美元獎金題目——相比擬的結果。他指出準黎曼假設是 722 項成果中唯一達到那個重要層級的問題。
Saha 在 X 上寫道:
Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026
此次發布也未達到高等研究院一個顧問小組於 9 月 29 日提出的建議。該小組建議披露模型名稱、提示詞、摘要版思維鏈、每項結果所耗時間與運算成本。OpenAI 提供了平均運算數據和 10 份推理摘要,但未提供提示詞。該公司表示仍在努力以負責任的方式釋出模型。
多倫多大學數學家 Daniel Litt 則持相反立場,認為沒有理由要求 OpenAI 對這些數學問題的答案保密。
Anthropic 上個月採取了不同的做法,將一份經 Lean 驗證的費馬最後定理證明全部 1,300 萬行程式碼公開在 GitHub 上。該工作形式化了 Andrew Wiles 於 1995 年發表的定理,而非提出新的數學結果。這兩次發布凸顯了業界在披露策略上的分歧:一邊是對已知定理完整、經機器驗證的證明,另一邊則是僅有部分形式化驗證的大量新主張n
OpenAI 表示將在取得 Lean 形式化後陸續補充。目前,722 份手稿中有 162 份具備形式化的主結果。其餘手稿的地位現在取決於研究人員表示最需要的東西:模型的釋出、底層提示詞,以及對其餘手稿的獨立形式化。