好傢夥，OpenAI
剛剛直接給數學界端上了 722 篇論文。
剛剛直接給數學界端上了 722 篇論文。這是 OpenAI 一款內部未發布模型產出的數學成果，已經打包放進了 GitHub。這些手稿歸為 372 組成果，供所有人查看。
APPSO 先給你把重點劃出來：
722 篇手稿，歸為 372 組成果。 同一組可能包含主結果、配套論證、推論和不同證明，不能直接理解成解決了 722 道獨立難題。
重點課題涉及准黎曼猜想、唯一博弈猜想、霍奇猜想的特殊情形，以及自由群因子問題。 光看題目，含金量已經拉滿。
結果處於不同驗證階段。 部分附有 Lean 形式化材料，公開上傳也不意味著全部完成學界審查。
論文公開了，模型還沒開放。 人類現在拿到了研究材料，接下來要逐項檢驗、理解和使用它們。
GitHub 🔗https://github.com/openai/math
奧特曼則發文表示：
則發文表示：我們正在進入一個發現的新時代。
OpenAI 的說法，現有數學評測快刷滿了，於是把更多開放研究問題搬上考卷。模型接到約 4000 個問題，輸出經過歸組和重要性篩選，形成了這份目錄。
每項結果，平均消耗相當於約三小時 ChatGPT Pro 思考的算力。
看這架勢，奧特曼怕是想讓數學家們看完目錄，先癱坐在地上緩一緩。
准黎曼猜想，這次到底走到了哪一步？
OpenAI 發布這個論文包後，羅格斯大學數學教授 Alex Kontorovich 在 X 上的反應，問號和感嘆號都快裝不下了：
在 X 上的反應，問號和感嘆號都快裝不下了：准黎曼猜想？！？你在開玩笑嗎？如果這是人類做出來的，立刻就是一枚菲爾茲獎，毫無疑問。
，毫無疑問。
黎曼 ζ 函數與素數的分布密切相關。它在某些位置的值為零，這些「零點」的位置，會影響我們能多精確地描述素數的分布。
黎曼猜想認為，所有非平凡零點都落在實部等於 1/2 的直線上。這次手稿提出的結論是：實部大於 7/8 的區域，沒有零點。
Kontorovich 解釋，過去在臨界帶靠近實部 1 的一側，已知的無零點區域會隨著虛部升高越收越窄。他原本以為，能把這片區域拓寬一點，就已經是重大突破。
這次手稿給出的，卻是一條寬度固定、無限延伸的條帶。在 0 到 1 的臨界帶內，7/8 右側整片區域都被划進了「零點禁區」。倉庫提供了相關 Lean 形式化材料。
「准」字必須要加上，完整的黎曼猜想還沒有因此解決。
唯一博弈猜想，多少有點給算法優化潑冷水的意思。
很多計算問題，想快速拿到最優答案太難，只好爭取一個足夠好的近似答案。比如 Max-Cut：把關係網裡的點分成兩撥，儘量讓更多連線跨過兩撥之間。
：把關係網裡的點分成兩撥，儘量讓更多連線跨過兩撥之間。這組論文宣稱證明了唯一博弈猜想，並給出 Max-Cut 等問題的近似難度界限。若證明成立，在 P≠NP 這個尚未證實的前提下，高效算法在一般輸入上的最壞情況近似保證，就無法突破相應界限。具體數據或特殊結構上的表現，仍可能繼續改善。
翻到霍奇猜想，又是一個千禧年大獎難題。它關心複雜幾何空間中的某類特徵，能否由多項式方程定義的幾何部件來表達。
這次論文處理的是 CM 阿貝爾簇上的有理霍奇猜想，一個特殊而重要的類別。
完整的霍奇猜想依然不能就此宣布解決。這項成果目前也未列出配套 Lean 形式化。
自由群因子的問題，讀起來有點繞。
想像用兩套基礎操作，分別搭出龐大的數學運算系統。一個從兩個生成元出發，另一個從三個出發：最終形成的算子代數，結構上能不能完全對應？
論文給出的答案是可以，範圍還覆蓋了所有參數大於 1 的插值自由群因子，包括無窮參數情形。倉庫提供了相關 Lean 形式化材料。這裡相同的是構造出的算子代數結構，原來的自由群並沒有因此變成同一個群。
談到 AI 給數學界帶來的變化，美國西北大學數學家 Bryna Kra 在此次發布前接受 WIRED 採訪時說：
這是個令人不安的時刻，但也著實令人興奮。
Lean 都附上了，能開香檳了嗎？
按公開目錄統計，162 篇手稿的主結論附有 Lean 形式化材料。
所謂形式化，就是把命題、定義和證明寫成有嚴格規則的代碼，再交給電腦檢查。Lean 按邏輯規則核對推導，證明不能靠一句「顯然成立」糊過去。驗證時還要檢查它依賴的公理和假設，以及有沒有尚未補齊的證明。
康奈爾大學數學副教授 Daniel Halpern-Leistner 正在開發工具，把自動形式化接入數學家的日常研究，他前兩天在採訪中說：
現在這件事顯得非常緊迫，因為用自然語言寫出的論證正大量湧來。
不過，機器首先得拿對題目。若把「所有情況都成立」寫成「滿足額外條件才成立」，它檢查的就是後一個命題。代碼里的定義是否對應原問題，需要人來核對。
覆蓋範圍也有區別。准黎曼成果的說明就註明，論文後續應用不在該形式化範圍內。因此，「主結論附有 Lean 材料」還不能給整篇論文的所有結論蓋章。
OpenAI 也承認，部分未形式化結果可能存在問題，會繼續修訂。
准黎曼成果的形式化範圍說明
的形式化範圍說明即便推導經得起檢查，數學家還要弄清楚，這個方法為什麼有效、能搬到哪些問題上。
這兩個月，數學家和 OpenAI 沒少拉扯
OpenAI 這兩個月可算是跟數學家槓上了。
8 月，OpenAI 召集約 40 位數學家，暗示模型已解出數百道題。大家要求發表能供同行研究的論文。有與會者稱，公司保證不會一次性發布；OpenAI 發言人則表示，不知道有過這個保證。
連有沒有答應過，雙方都沒對上。
9 月 8 日，OpenAI 公布納維—斯托克斯千禧年大獎問題的解答主張，附上論文和 Lean 形式化證明。三天後，陶哲軒等 25 位菲爾茲獎得主作為最初聯署者，發表了關於 AI 與數學目標錯位的公開信。
他們批評 AI 公司把攻克開放問題當作模型評測目標，卻忽略了理解、引用和人才培養。數學家研究難題，還希望從中長出新概念、新方法。答案來得太快，這些工作未必跟得上。
也有菲爾茲獎得主沒有簽字。Timothy Gowers 在 9 月 17 日的部落格里設想，即使一年湧來 1000 項重要成果，數學家仍可以按領域分工消化。這會是項大工程，但未必做不到。他更擔心，支撐這些研究和理解工作的學術環境會被破壞。
隨後，獨立數學與 AI 諮詢小組 AGMAI 成立。OpenAI 在 9 月 21 日的公告中回應了公開信。它還聲稱，一款從 8 月 28 日開始訓練的新內部模型，已解決「100 多個長期開放問題」。不過，公告並未附上這批成果的逐項清單和證明。
9 月 29 日，諮詢小組給出發布建議：完善引用，寫成便於同行理解的論文，放到獨立學術存檔平台，並資助人類消化這些成果。它還明確反對繼續用科學共同體無法訪問的專有模型測試前沿數學問題。
今天，OpenAI 甩出 722 篇手稿放上 GitHub。OpenAI 設置了修訂和引用規範，公開 10 份推理摘要，承諾資助相關研討會，也表示仍在尋找符合建議的社區託管方式。
同一天，AGMAI 專門說明，提供建議不等於評定成果的影響，更不代表認可其產生過程。數學家需要公平獲取工具和算力，才能選擇自己的研究問題。
目前，生成這些成果的模型仍未向公眾開放。研究者可以下載答案，卻還不能普遍使用同一款工具，接著問下去。
更值得期待的下一步，是數學家也能用上這款模型，拿自己的問題去驗證。
否則，大家可能忙著消化 AI 公司選好的題目，自己的研究還在排隊。原本盼著來個科研助手，最後卻給 AI 當起了助理，這就有點反客為主了。
更讓 APPSO 好奇的是，看完這些 AI 寫的論文，陶哲軒等數學家有什麼反應？
