OpenAI 公開 722 份 AI 生成數學論文：未釋出前沿模型一次倒出 90 個未解難題

OpenAI 10 月 6 日在自家研究部落格發布「Sharing AI progress in mathematics」，一次把內部未釋出的「前沿模型」(frontier model) 跑出的 722 份數學論文、372 個結果家族、橫跨 377 個開放問題，連同 Lean 4 形式化證明與模型推理摘要，全部丟上 GitHub。這是繼 8 月「Ten advances」之後，OpenAI 第二次把 AI 數學研究的成果大規模倒出來。但跟上個月不同的是，這次 OpenAI 明確承認「我們不釋出模型」。

編按：本文綜合整理自 OpenAI 官方部落格、GitHub openai/math 倉庫、The Verge 報導、WIRED 評論、NYT 報導與 Quanta Magazine，並加入 Siami 編輯部觀點與分析。

這次丟出了什麼

OpenAI 把這次釋出定位成「負責任的數學成果分享」嘗試，跟 9 月在普林斯頓高等研究院 (Institute for Advanced Study) 設立、由 Terence Tao 等數學家組成的獨立 Advisory Group on Mathematics and Artificial Intelligence 合作設計釋出流程。具體交付物：

722 份預印本 (preprints)，全部放在 github.com/openai/math，每份都有獨立的 LaTeX 源碼與 metadata
372 個結果家族，分群為幾何、數論、組合、機率、偏微分方程等多個子領域
Lean 4 形式化檢查 — 部分證明有對應的 Lean 證明書，可被計算機獨立驗證
10 段模型推理摘要 — 從「模型怎麼想到這個解」到「它卡在哪裡」都記錄下來
4,000 個嘗試問題的統計 — OpenAI 公開了模型在哪些問題上失敗、哪些成功，方便後續研究者重現平均每個結果消耗的算力，大約是 ChatGPT Pro 思考模式 3 小時的等效計算量。

為什麼這件事重要這不是「OpenAI 又發了個厲害模型」的科技新聞，這是 AI 與數學社群的關係進入新階段的標誌。第一，這是第一次有人把 AI 生成的數百份研究結果以「可審查」形式公開。以前 AI 給數學家的東西是「對話框裡的幾行字」或「一份 PDF 摘要」，社群要嘛信、要嘛不信，沒有灰色地帶。這次 OpenAI 押的是「我們給你源碼、給你 Lean 證明、給你統計，你來審」。第二，模型本身繼續被鎖在 OpenAI 內部。這跟 Google DeepMind 對 AlphaProof 的處理方式一樣，但跟 Meta 開源 Llama 路線相反。社群拿到的是「論文級成果」，但「產生這些成果的工具」被當成商業機密。第三，這是 OpenAI 第一次正面承認「負責任揭露」是一個他們必須單獨處理的問題。9 月 Advisory Group 成立、10 月這次釋出，OpenAI 想證明他們可以跟頂尖數學家合作，而不是繞過他們。

數據解讀與爭議

722 份論文、377 個問題，看起來很漂亮，但魔鬼藏在 Lean 形式化覆蓋率裡：

真正有 完整 Lean 4 形式化證明書 的，只有延續 8 月 ten-proofs 倉庫的那 10 個
其餘 700 多份是「OpenAI 說是這樣，附上論文 + 推理摘要，但沒有機器可驗證的證明」
等於 700 多份「待同儕審查的 AI 主張」這個落差正是頂尖數學家怒火的核心。WIRED 引述一位受訪者用「mobster behavior」(暴徒行為) 形容 AI 大廠目前的做法，9 月已有一封 25 位數學家連署的公開信警告 AI 實驗室威脅到他們的智識工作。Economist 9 月報導同樣以「頂尖數學家被 OpenAI 的方法惹毛」為題。另一個值得注意的點是 GitHub 託管策略。OpenAI 沒有用 arXiv 這種數學社群已經熟悉的預印本平台，而是選了 GitHub。這被解讀為「我們要的是工程師的迭代速度，不是學術界的審查紀律」。

社群反應：信用、版權、優先權這次釋出撞上三條已經存在的紅線：

Tristan Buckmaster 私訊外洩爭議（9 月爆出，OpenAI 被指控把數學家跟 Codex 對話的內容挪用成訓練資料並產出「解法」）
Navier–Stokes 千禧年問題解法（9 月 8 日公告，當時就被質疑在「公開前沒讓領域專家先看」）
OpenAI 安全主管辭職信（10 月初 Steven Adler 公開信警告 AI 產業文化「徹底壞了」）

Hacker News 討論串 item?id=49984923 上，最高分留言直接點名：「把幾百份未經嚴格同儕審查的數學論文灌進 GitHub，又不釋出產生它們的模型，這算什麼負責任揭露？」

Advisory Group 的存在是好開始，但 Terry Tao 9 月在自己的部落格寫得很清楚：這個機制要有效，前提是「AI 公司願意在發表前先讓顧問看結果」。現在的模式是「先 dump、後道歉」，順序完全反了。

Siami 觀點這次釋出有兩個值得肯定的設計選擇：

公開推理摘要與嘗試統計 — 這在 AI 研究領域非常少見，多數公司只給「成功案例」。OpenAI 願意讓社群看「模型卡在哪裡」是難得的透明度
預先設立 Advisory Group 處理 release 流程 — 即使顧問影響力被質疑，至少制度先架起來了但有兩個結構性問題沒解決：
沒有 Lean 證明書的 700 多份論文，實務上等同「不可驗證」。數學社群一年能仔細審的論文本來就少於 1000 篇，把 700 多份 AI 主張灌進 pipeline 不是加速，是把審查義務外包給已經過載的學術系統
模型未釋出 = 結果無法重現。這違反了科學發表的最低標準。OpenAI 可以說「我們怕模型被濫用」，但 722 份論文的可重現性就因此歸零

AI 進入數學研究這件事，9 月 Navier–Stokes 解法時已經吵過一輪，10 月 722 份的「GitHub dump」是第二輪。如果 OpenAI 想要的不是「在 Hacker News 上被罵」，而是「被數學社群當成合作對象」，他們要做的下一步很明確：把模型開源（至少對經審查的學術機構開放 API），或者把剩下 712 份也補上 Lean 證明書。否則這個倉庫就只是「OpenAI 的公關戰場」，不是「AI for Math 的里程碑」。

技術補充：Lean 形式化是什麼

Lean 是一個由 Microsoft Research 與卡內基美隆大學維護的交互式定理證明器 (interactive theorem prover)。數學家可以在 Lean 裡把證明寫成程式，Lean 的核心 (kernel) 會獨立檢查每一步推論是否合乎邏輯。這對 AI 數學研究的意義是：如果一個「AI 解法」有對應的 Lean 證明書，那這個解法的正確性不再依賴人類同儕審查 — 機器已經先檢查過了。這也是為什麼 8 月 ten-proofs 倉庫被視為「AI for Math 的第一個真正里程碑」，而 10 月這 712 份沒附 Lean 證明的論文，數學社群反應就冷淡得多。