OpenAI 在 GitHub 上再發布 372 項來自未公開 Astra 模型的數學成果

新聞摘要

OpenAI 已在 GitHub 上發布了第二批規模更大的數學成果：共 372 項主張，全部歸功於 Astra——該公司稱之為下一次重大發布的內部模型。根據美國東部時間 2026 年 10 月 6 日的報導，每一項成果據稱都解決或大幅推進了數學或理論電腦科學中的一個未解問題。其中許多成果附帶以 Lean 程式語言撰寫、可由機器檢驗的證明，但由於模型本身尚未發布，外部研究人員目前還無法重現這些成果的產生過程。

OpenAI 發布了什麼

此次新發布距 OpenAI 首次公告約兩個月，首篇名為〈數學與理論電腦科學的十項進展〉的公告發表於美國東部時間 2026 年 8 月 1 日。第一批成果涵蓋八個領域中的十個長期未解問題，包括群論、算子代數、編碼理論與極值組合學。當時隨公告一併公開的還有 249 頁的手稿，以及存放於公開 GitHub 儲存庫中的 Lean 4 驗證憑證；OpenAI 表示，依其 API 費率計算，所使用的 token 成本約為 2,000 美元。

10 月的這批成果數量是首批的 37 倍以上。報導指出共有 372 項成果，相關主張包括四維 Kakeya 猜想的解答、對若干常用電腦演算法的改進，以及與黎曼猜想相關的部分進展。OpenAI 表示，幾乎每項成果都來自向單一 AI 代理發出的單一提示詞。該公司僅揭露了平均運算時間，並未公布個別提示詞或每項成果的具體運算量。

為什麼 Lean 證明很重要

Lean 是一款證明輔助工具：一種能以機械方式檢查證明中每個邏輯步驟的程式。當一項成果在 Lean 中被形式化後，讀者就不必盲目信任作者。軟體要嘛接受該證明，要嘛予以駁回。《科學人》雜誌報導指出，經過 Lean 驗證的證明幾乎可以確定是正確的。

這是說明電腦驗證數學如何運作的一個實用教學範例。Lean 證明能保證某個命題是由其假設推導而來，但無法保證該命題的形式化意義與人類讀者的理解一致，也完全無法說明這個證明是如何被發現的。

數學家們怎麼說

各界反應不一。麻省理工學院的 Andrew Sutherland 表示，在模型發布且他人能夠重現這些工作之前，關於用單一代理一次提示就解決問題的說法應視為未經證實。多倫多大學的 Daniel Litt 認為，如果學術界想要這些問題的答案，就沒有理由依賴某家公司來壟斷得出答案的工具。Terence Tao 則批評 AI 實驗室目前產出成果的速度，稱其「瘋狂至極」。

《科學人》雜誌也指出，OpenAI 並未完全遵循獨立顧問小組的建議，部分成果可能經過多次嘗試才得出，而且有些內容連 OpenAI 自家的數學家都尚未完全理解。要審閱數百項成果，對人類專家社群而言是一項沉重的負擔。

第一批成果引發的引用爭議

美國東部時間 2026 年 8 月 6 日，《科學人》雜誌報導，部分專家指出 Astra 在前十項成果中有兩項未能適當註明先前研究的出處。葉史瓦大學的 Stephen Miller 表示，他 2016 年研究中關於球堆積的論證被當作原創成果呈現。另一項關於群論中 soficity 的成果，據稱結合了 2016 年與 2019 年發表論文中的想法，卻未給予充分引用。劍橋大學的 Francesco Fournier-Facio 表示，該公告忽略了近期關鍵的研究進展；而德勒斯登工業大學的 Andreas Thom 則形容該群論證明既有創意，同時又相當基礎。

OpenAI 承認了這些問題。一位發言人表示，公司將依照標準學術慣例，於當週進行小幅更新。

接下來該關注什麼

有三個問題將決定這些成果如何被外界接受。第一，372 項主張中有多少能通過獨立審查並被已發表文獻所採納。第二，OpenAI 是否會開放 Astra，讓「單一提示詞即可得出成果」的說法得以驗證。第三，該領域是否會建立起引用先前研究與標註 AI 輔助發現的規範。對學生與教育工作者而言，這次事件既展現了形式化驗證的潛力，也凸顯了人類同儕審查依然不可或缺。

資料來源說明

研究過程中無法取得 The Verge 針對本次發布的報導，因此上述細節均來自《科學人》雜誌及其他關於 OpenAI 八月與十月公告的報導。有關具體成果的主張皆出自 OpenAI，並非全部經過獨立證實。