OpenAI 本週突然向數學界投放了近 400 項 AI 生成的數學結果,分佈在 700 多份手稿中,覆蓋組合數學、多個幾何分支、數論、理論電腦科學、代數、拓撲、機率與統計力學以及數學物理等方向。據 The Verge 報道,超過 36 位數學家在受訪時用「驚人」「壓倒性」「前所未有」「超現實」「純粹的瘋狂」來形容自己的反應。這批材料的體量之大,甚至讓 OpenAI 自己都覺得有必要釋出一份導航指南,幫助研究者在這座龐大的 GitHub 倉庫中找路。
即便只是做初步評估也異常困難。多數受訪數學家表示,在釋出後的數小時乃至數天裡,他們仍在努力消化全部內容;有幾位說,光是過一遍約 40 頁的目錄與摘要就花了將近一小時。康涅狄格大學數學教授 Álvaro Lozano-Robledo 表示,僅僅瀏覽全部摘要就已經讓人不堪重負。
手稿中夾雜著用 Lean 寫成的形式化內容。Lean 是一種程式語言兼證明助手,可讓結果被計算驗證。這類形式化在此前評估 OpenAI 的數學宣告時發揮過關鍵作用,能讓研究者即便不完全理解論證過程,也對某個宣告的邏輯正確性抱有信心。有研究者形容,如果這些 AI 現在消失,就像外星人來到地球后又離開,數學界接下來十年都會用來研究這批東西、試圖理解全部內容。
但每項結果被驗證的程度差異極大。OpenAI 在 GitHub 上承認,這些結果處於「不同的驗證階段」,「許多但並非全部手稿已被形式化」。截至報道時,這批手稿中不到一半似乎有形式化描述。OpenAI 表示,719 份手稿中只有 300 項主要結果完成了形式化,約佔 42%,並稱會隨著獲得更多形式化內容而更新倉庫。
多位數學家向 The Verge 抱怨形式化不足,尤其是在結果數量如此龐大的情況下,並強調即便有 Lean 程式碼伴隨,評估也並非瞬時完成。研究者必須核對形式化內容是否真的證明了結果所聲稱的東西,這又是一個耗時的過程。有幾位翻查論文的人表示,即便提供了可被計算機驗證的證明,質量也不一致,而且被驗證的陳述並不總能與隨附手稿中的宣告嚴絲合縫地對應。
倫敦帝國理工學院數學教授 Kevin Buzzard 表示,他在自己從事的代數數論領域識別出大量定理,其中只有大約 6 個立刻「脫穎而出」,而這些定理中幾乎沒有幾個看起來在 Lean 中完成了形式化驗證。他的困境頗具代表性:要麼去讀可能並不正確的「垃圾內容」,要麼等別人去讀,要麼等有人把它們形式化,之後才能確定結果是否正確。
Buzzard 對 AI「垃圾內容」的擔憂並非孤例。這個詞是低質量、常常出錯的 AI 生成材料的簡稱,這類內容正越來越多地出現在網上乃至現實世界中,包括學術論文。數學家們告訴 The Verge,近年來用 ChatGPT 和 Claude 等工具生成的此類材料大幅增加,其中許多內容令人費解、難以閱讀,對主題的理解也很有限,在引用其他研究者成果方面尤其粗糙。OpenAI 此前的數學寫作就曾因草率而受到專家廣泛批評,尤其是署名與出處標註糟糕甚至完全缺失。
在釋出前與 The Verge 的交流中,多位研究者已把即將到來的論文洪流稱為「slopocalypse」(垃圾內容末日)或類似說法。這場擔憂中的「末日」是否真的成為現實,很難判斷,很大程度上是因為材料數量令人眼花繚亂。早期跡象顯示,OpenAI 這一次對論文更為用心,至少對其中一部分是如此。有幾位數學家表示,第一印象遠好於他們的預期,不過他們也承認,鑑於該公司此前出版物質量堪憂,這個門檻本來就不高。
從產業視角看,這次釋出把兩個問題同時擺上檯面。其一是能力問題:如果這批結果中確有大量成立的新定理,那意味著前沿模型在形式化推理與數學發現上的能力又向前邁了一步,這對 AI 在科研、工程與藥物研發等需要嚴密推理的場景中的可信度是正面訊號。其二是可信度問題:形式化比例僅約四成、質量參差、宣告與驗證內容未必對齊,意味著「AI 能產出數學成果」與「這些成果可被數學界採信」之間仍隔著巨大的驗證鴻溝。
對關注 AI 產業的人而言,這件事的意義不只在數學本身。它是一次關於 AI 生成內容如何進入嚴肅知識生產體系的壓力測試:當產出速度遠超人類審閱速度時,驗證機制、署名規範與學術信用體系都會承壓。OpenAI 選擇繼續向前推進,而數學界則要花數年時間,從海量手稿中分辨哪些是真正的成果、哪些只是看似合理的「垃圾內容」。這一分工本身,或許就是 AI 時代科研生態正在形成的新常態。