OpenAI 發表了 722 項由 AI 推導出的數學成果。數學家正追問：功勞該歸誰？

OpenAI 發布了一批由內部前沿模型產生的數學成果，同時公開了一個儲存庫，內含許多證明的 Lean 形式化，以及修訂與引用的相關規範。這份發布說明了 722 項成果，其中 162 項經過機器驗證。

外界的反應，與其說是在意這些數學是否正確，不如說是在意「驗證」究竟能帶來什麼，以及這些成果究竟屬於誰。

Lean 驗證了什麼，又沒驗證什麼

Lean 是一套證明助理。它會依照既定的公理，機械式地驗證形式論證的每一步，這意味著一份通過檢查的證明不可能存在邏輯漏洞。只要它能編譯通過，該論證就能從前提推導出來。

這是個很強的保證，但範圍也很窄。證明助理驗證的是形式陳述能否被推導出來，而不是驗證形式陳述真的表達了隨附文字所宣稱的內容。仍然必須有人逐一閱讀這 162 項機器檢查過的成果，確認該 Lean 檔案所編碼的，確實是某個人以為的那個定理。形式化是一個翻譯步驟，而翻譯會走樣。

其餘 560 項成果沒有這類檢查，也就是說，這份公開發布把兩種截然不同的證據等級混在一起。報導「722 項成果，162 項已驗證」比只報總數更誠實，但這也意味著標題數字把已驗證的子集誇大了約四倍半。

功勞歸屬問題有了新的樣貌

打從數學這門學科存在以來，數學家就一直在爭論功勞該怎麼分配，而爭論的通常是誰提出了問題、誰找到了關鍵步驟、誰把它寫出來。AI 產生的成果則帶來了一個前所未見的版本。

如果一個模型證明了某個長年未解的開放問題，作者是誰？是模型本身嗎——但依現行著作權框架，模型也不能是法律上的作者？是下提示詞的研究者？是整理問題清單的團隊？還是訓練了模型、卻不釋出權重的機構？

OpenAI 表示正朝負責任地釋出底層模型的方向努力。但在那之前，社群無法在同一個系統上重現這些成果，無法檢視訓練資料，也無法評估模型的成功是否取決於訓練期間看過相關問題。發表與可重現性是兩種不同的承諾，而這份發布只兌現了前者。

數學領域還有一個特有的複雜之處：這個領域的功勞歸屬是建立在理解之上的。一份證明的功勞，有一部分來自它引進的想法，而數學想法傳播的方式，是靠人們閱讀它、發現它有用，然後加以延伸。一份沒有人完全理解的機器產生證明，是無法以這種方式傳播的成果。它可以被引用，卻不容易被承繼發展。

還有一種實際的不對稱，將在未來許多年讓同儕審查變得複雜。一位人類數學家發表了有瑕疵的證明，一般會被理解為犯了誠實的錯誤，其名譽後果是相稱的。一個模型發表 722 項成果，有些正確、有些不正確，產生的是一批作品，其中正確與錯誤的比例本身無人知曉，而且沒有人能為錯誤的那些負責。期刊的運作機制，並不是為了處理作者身分分散、錯誤率是一種分布而非單一事件的投稿。

引用問題也隨之而來。數學的進展取決於知道哪些既有成果可以信賴。一項已在 Lean 中通過機器檢查的成果是強而有力的候選；而一項由模型提出、無人審查的成果則不是。把這兩類混在同一次發布中，反而讓兩者都更難被承繼利用。

同一天的另一則故事

OpenAI 的數學發布，出現在充滿第一方說法、卻少有第三方驗證的一週裡。

Mistral 推出 Large 4，一個一兆參數的模型，被定位為西方對開放權重中國系統最強的回應，其基準比較被一個回覆串逐行對照 Artificial Analysis 公布的數據，結果被找出問題——具體來說，是指控它挑選了競爭對手的特定變體來美化比較，並錯誤陳述了一項已公布的第三方數字。

Reflection 推出 Beam，一個瞄準同一戰場的開放權重模型，權重將於本月稍晚釋出。

而 Anthropic 則擴大了一款能找出軟體漏洞的模型的使用範圍，同樣帶著自家的第一方數字。

這一週呈現的模式是：能力宣稱到來的速度，快過查核它們的能力。arXiv 對同一股壓力的另一種表現作出回應，將投稿者上限訂為每月兩篇論文——此前它在九月收到破紀錄的 40,363 篇投稿，是兩年前的兩倍。

競爭的關鍵在於讓各種宣稱變得可用

有一種關於 AI 與數學的故事版本，被框成記分板：一個模型能終結多少個開放問題。更有用的框架，是思考什麼能讓一項成果被研究社群所用，而這牽涉到幾件模型發布本身不會提供的事。

審查者需要理解這個論證。功勞歸屬必須可追溯。其他研究者必須能在不重新推導的情況下承繼這項成果。而更廣大的社群，需要對產出該成果的系統有足夠的取用權限，才能自行測試。

最後一點，正是這次發布止步之處。一批由其他人都無法執行的系統所產生的成果，更接近一次示範，而不是一份貢獻。它展示了什麼是可能的，卻沒有交給這個領域任何可以獨立承繼的東西。

數學並不是這場轉型中最難的部分。難的是 AI 的能力如今已跑在那些為了驗證它而存在的機構之前（同儕審查、基準複製、作者規範、引用慣例），而這些機構是以人類的時間尺度在運作。一個模型可以在一次訓練執行中產生 722 項成果。但要釐清其中哪些重要、誰值得獲得功勞、以及它們會帶來什麼後續，仍然得以年為單位來衡量。

有一種對立觀點值得一提，因為它並非不合理。一份能編譯通過的形式證明就是證明，不管產出它的是誰或什麼。數學向來是憑成果本身的價值、而非其來源來接受成果；如果 Lean 驗證了某個論證，那個論證就成立。在這種觀點下，功勞之爭是這個領域應該以尋常方式解決的社會學問題，而堅持可重現性，等於要求一種人類數學家從未被要求提供的取用權限。沒有人會要求人類作者公開自己的思考過程。

反駁則是：人類作者可以被要求解釋自己的工作，而理解正存在於解釋之中。一份沒有附帶解釋的證明，是一個恰好有已驗證輸出的黑箱。這個領域可以引用它，卻無法教它——即使該定理為真，這仍是一種真實的損失。

這一週歸納出的實用建議，適用於任何採購 AI 能力的人，而不限於數學：要求看到證據、授權許可，以及從成功示範走向可重複工作的路徑。基準測試結果與可運作的系統是兩種不同的產物，而兩者之間的落差，正是意外藏身之處。