機器之心編輯部
就在今天早上，AI 圈與數學圈真的炸鍋了，很多研究者與網友真的癱坐在椅子上，被智慧爆炸所震撼。
很難以想像，這個 GitHub 倉庫裡放的不是一、兩個重量級數學成果，而是足足 722 個！
這是一份數學論文清單：722 篇手稿，歸入 372 個成果族，全部由一個尚未發布的內部前沿模型產出。
清單上的名字，足以讓任何讀過研究生數學課程的人停下來多看幾眼：準黎曼猜想、四維掛谷猜想、唯一遊戲猜想、自由群因子同構問題、有理數域上的希爾伯特第十問題、CM 阿貝爾簇的霍奇猜想、馬勒猜想……這些問題裡，有的懸置了半個世紀以上，有的曾是菲爾茲獎等級工作的延伸方向。
Sam Altman 表示我們正在進入一個大發現的新時代。
一次爆炸性發布
按照 OpenAI 的說法，這批成果來自對內部模型的數學能力評估。
由於模型在既有數學評測上的表現已經飽和，團隊把評估擴展到開放研究問題上，其中部分成果建立在模型此前產出的結果之上。整個評估過程中，模型被餵了約 4000 個研究問題；把輸出按相關性歸併為成果族、再按「足夠重要」的門檻篩選之後，留下現在這 372 族、722 篇手稿。
一個「成果族」通常包含一個主結果，以及配套論證、推論或替代證明。按 OpenAI 自己的學科標註，這 372 族涵蓋 17 個方向，數量最多的是理論電腦科學（40 族）、組合數學（37 族）、代數與複幾何（36 族）和數論（31 族），其後是機率與統計力學、微分幾何、數學物理、算子代數等；數理邏輯最少，也有 6 族。
算力方面，OpenAI 稱：絕大多數結果走的是同一套固定流程，平均每個結果消耗約相當於 3 小時 ChatGPT Pro 思考的算力。
另一個值得留意的細節是，手稿的資料夾以日期結尾，幾乎全部集中在 9 月 23 日至 10 月 5 日之間，其中 9 月 23 日和 24 日兩天就各有近 200 篇。換句話說，這份清單的主體，似乎是在不到兩週的時間裡批次輸出。
與論文一起放出的，還有三類「證明工件」：Lean 形式化證明、10 份模型推理過程的精簡摘要，以及計算量與嘗試問題數的統計。按我們對倉庫目錄的統計，372 族中有 235 族附帶了 Lean 形式化說明頁，約占六成三。
但 OpenAI 同樣坦承，並非所有手稿都完成了形式化，未形式化的結果「可能存在問題」，團隊會盡快修正並持續補充。
目前，該專案的 Star 數正在瘋狂上漲中，僅僅三個小時，已經突破了 2k。
倉庫地址：https://github.com/openai/math
黎曼與掛谷
在 722 篇手稿中，最先在社群媒體上洗版的是編號 003：準黎曼猜想。
黎曼猜想斷言，黎曼 zeta 函數的所有非平凡零點都落在實部為 1/2 的直線上。這個目標太遠，數論學家退而求其次，提出了「準黎曼猜想」：哪怕證明存在某個小於 1 的常數 θ，使得實部大於 θ 的整個半平面裡都沒有零點，也是巨大進展。
一百多年來，人們能證明的零點自由區域都會隨著虛部增大而越來越貼近實部為 1 的那條線，始終沒能「撐」出一條固定寬度的垂直帶。OpenAI 這次給出的結論是 θ = 7/8，對 zeta 函數和所有狄利克雷 L 函數一致成立，並且已經給出 Lean 形式化。配套論文還給出了 Landau–Siegel 零點的一個一致排除結果。
另一個引發熱議的是編號 074：掛谷問題。
就在今年 7 月 23 日，王虹憑藉與 Joshua Zahl 在 2025 年完成的三維掛谷集合猜想證明獲得菲爾茲獎，成為史上第三位獲此殊榮的女性數學家；彼時《量子雜誌》盤點的「下一步」裡，四維掛谷猜想仍赫然在列。
OpenAI 清單裡的這一族同時聲稱解決了三維掛谷「極大函數」猜想和四維的豪斯多夫維數猜想。
重量級的成果遠不止這兩項。
• 理論電腦科學方向，編號 102 聲稱證明了 Subhash Khot 於 2002 年提出的唯一遊戲猜想，並據此一口氣給出 Max-Cut、頂點覆蓋等經典問題的最佳近似難度門檻；
• 代數幾何方向，編號 032 聲稱對所有複 CM 阿貝爾簇證明了有理霍奇猜想；
• 數論方向，編號 002 與 006 合起來，給出了每條有理橢圓曲線的一個密度為一的二次扭曲族上完整的 BSD 公式；編號 004 則對有理數域上的希爾伯特第十問題給出了否定解答。
這三項都牽涉千禧年大獎難題或二十世紀的標誌性問題。
算子代數方向，編號 287 聲稱解決了自由群因子同構問題，結論是不同秩的自由群因子彼此同構，附帶 Lean 形式化。
此外，清單中還有證明 π 的無理性測度恰為 2、卡塔蘭常數為無理數、馬勒猜想在所有維數成立、平面不能用五種顏色完成單位距離染色等結果，也有對 Kaplansky 零因子猜想、Hadwiger 猜想的反例構造。
作為補充，下面是前 OpenAI 研究者 Will Depue 用 GPT 6 Pro 和 Fable 5.1 對過去三年的所有發現進行排名。其中藍色表示人類發現、紅色表示 AI 發現（10 月 6 日之前）、綠色表示來自 OpenAI/math repo 的 AI 發現。震撼的是，其中 81% 是今天才發布的。
一個神秘內部模型
整場發布裡，模型本身始終缺席。OpenAI 沒有公布它的名字，只在部落格中稱之為「內部前沿模型」，並表示正在推進其「負責任的發布」。
9 月 8 日，OpenAI 發布了 Navier-Stokes 公告。公告稱，一個「顯著強於 GPT-6 Astra」、8 月 28 日開始訓練且訓練仍在進行中的內部模型，用約 1 萬個並行代理、88 小時的工作，證明了三維不可壓縮流體在光滑外力作用下可以從靜止狀態出發、在有限時間內產生奇異點，並用 GPT-6 Astra 額外花了 17 小時完成 Lean 形式化。
相關連結：https://openai.com/zh-Hans-CN/index/navier-stokes-solution/
發布前夕，OpenAI 發言人就已證實，這個新內部模型已經解決了「數學大多數領域裡」超過 100 個長期懸而未決的問題。
數學家的群情激憤
過去兩個多月，AI 實驗室與數學家之間的摩擦壓力一路攀升。
8 月 1 日，OpenAI 公布下一代模型 Astra 在數學與理論電腦科學上的十項進展。僅幾天後便有數學家指出，其中證偽 Connes 剛性猜想的反例裡，有一個群不滿足所需條件。8 月 11 日，Anthropic 也披露其未發布模型在黎曼猜想相關方向取得進展。
據《連線》報導，在 8 月，OpenAI 私下召集了約 40 位數學家，討論如果 AI 在數學上超越人類該怎麼辦。
與會者稱，OpenAI 當時暗示其模型已經解決了數以百計的長期難題，並就如何發布徵求意見；有與會者稱公司還承諾不會一次性全部釋出，但 OpenAI 發言人表示「不知道」有過這樣的承諾。
西北大學數學家回憶，與會者的情緒是興奮與恐懼交織，大家當場提出，不要再像 8 月十道題一樣只靠部落格和推文發布，而要寫成論文，讓數學家能夠消化和使用這些結果。
據報導，OpenAI 是在聽到有人即將解出該問題的「傳聞」後，才調動數千個代理進行攻關。紐約大學的 Tristan Buckmaster 指控 OpenAI 搶跑了他與 Levent Alpöge 私下合作的工作，Alpöge 本人是 Anthropic 員工，兩人尚未發表成果，卻一直在使用 OpenAI 的工具輔助研究。
相關連結：https://www.wired.com/story/openai-is-pissing-off-a-bunch-of-mathematicians-again/
數學家表示，「人們覺得這些頭部 AI 公司有種黑幫式的行事作風。」
9 月 11 日，包括陶哲軒在內的 25 位菲爾茲獎得主聯署聲明。聲明認為，攻克名題本是推動概念理解的工具和代理指標，而倉促的公告留不出時間來寫好論文、做好引用，會帶來嚴重的署名與抄襲問題。
相關連結：https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/
在此之前，一份由 4000 多名數學家聯署的《萊頓宣言》已經要求 AI 公司遵守數學界的標準，內容涵蓋披露 AI 使用、同儕審查、引用前人工作和保持開放取用等，Bryna Kra 是起草者之一。
9 月 29 日，高等研究院（IAS）數學與人工智慧獨立諮詢小組在彙整了 600 多份社群問卷後，發布了一份 AI 生成數學成果的發布建議。這正是 OpenAI 此次在推文和部落格中特意援引的那份文件。
https://agmai.org/general-sep29/
IAS 的建議分兩步。
第一步是「初次發布」：實驗室要檢索並引用相關已有工作，把證明寫成符合傳統數學論文慣例的樣子；要公開模型名稱、提示詞、思維鏈摘要、耗時和運算成本估算；要盡可能形式化；要存放在「不受任何 AI 實驗室控制」的中立倉庫，帶持久識別碼與修改記錄；還要報告在可比問題上的失敗率。
第二步是「支援理解」：資助會議、研討會和闡釋性寫作，並向全球數學界提供廣泛、公平的模型存取。
拿這份清單對照，OpenAI 的答卷可以說是「有選擇地及格」。公開推理摘要、運算估計和嘗試問題數，承諾資助一系列圍繞 AI 重大成果的研討會和會議，承諾版本留痕、修訂以新版本發布，形式化做了六成以上。
不符合建議的地方也很多。尤其是未公開模型名稱。倉庫放在 OpenAI 自己的 GitHub 組織下，OpenAI 表示仍在探索社群託管的替代方案。OpenAI 也在部落格裡承認，未來的發布會在引用、數學闡述和呈現方式上繼續改進。
瓶頸從「證明」移到了「理解」
如果說 9 月的 Navier-Stokes 公告證明了 AI 能啃下一道最難的題，那麼這次發布證明的是另一件事：在相當寬的數學前沿上，產出可檢驗的新結果，已經可以按「每題幾小時」的節奏批次進行。
這讓陶哲軒在 9 月提出的那個判斷變得更加尖銳：真正的衝突不是人類推理對機器推理，反而是充沛的證明產出與稀缺的專家注意力之間的錯配。
372 個成果族裡，有 235 族帶有 Lean 證明，這確實大大降低了「證明是否正確」的驗證成本；但 Connes 剛性猜想的插曲已經提醒過所有人，形式化能保證推理無誤，卻不能自動保證被證明的命題就是數學家心裡那個命題。OpenAI 為每一族準備的 Lean 說明頁裡專門寫明「涵蓋到哪裡、沒涵蓋到哪裡」，比如準黎曼猜想一族就註明論文中後續的應用部分不在形式化範圍內，這本身就說明了陳述層面的核對仍然離不開人。
至於那些分量最重、卻尚未形式化的結果，比如四維掛谷、CM 阿貝爾簇的霍奇猜想、有理數域上的希爾伯特第十問題，接下來幾個月裡能否經受住專家逐行審讀，才是這次發布真正的成績單。
一個更值得追問的問題是：當新定理的供給不再稀缺，數學共同體要如何重新分配自己最寶貴的資源，也就是讀懂它們的時間？
Sam Altman 說我們正在進入一個發現的新時代。這句話的前半句，今天已經有了 722 份證據；後半句「發現」要真正成立，還需要人類把這些結果讀懂、接住，再傳下去。
參考連結
https://openai.com/index/sharing-ai-progress-in-mathematics/
https://github.com/openai/math/blob/main/lean/docs/003.md
https://quantamagazine.org/hong-wang-wins-2026-fields-medal-the-third-woman-ever-20260723
https://www.remio.ai/post/terence-tao-ai-math-warning-challenges-the-benchmark-race
© THE END
轉載請聯繫本帳號取得授權
投稿或尋求報導：liyazhou@jiqizhixin.com