OpenAI 在 GitHub 一次放出 722 篇數學手稿，全由一個沒名字、沒定價、也沒有 API 的內部模型生成。證明用的是可被電腦檢查的 Lean，但獨立核驗還跟不上。
OpenAI 丟出的 722 篇數學手稿是什麼
10 月 6 日，GitHub 上出現一個名為 openai/math 的倉庫，同一天 OpenAI 發表文章「Sharing AI progress in mathematics」。倉庫裡有 722 篇數學手稿，歸進 372 個研究群組（families）。一個「群組」指的是一組相關的論文，可能包含一個主要結果，加上配套論證、推論，或另一套證明方式。
這些手稿涵蓋純數學、理論計算機科學與數學物理。OpenAI 說，這些結果解決了、或實質推進了數學與理論計算機科學裡一些重要的未解問題。
真正特別的是「作者」。這 722 篇不是人類數學家寫的，而是由 OpenAI 一個對外未命名的內部前沿模型生成。這個模型沒有對外開放、沒有定價、也沒有可用 API，外界看不到它、也摸不到它。
Lean 是什麼，為什麼它讓證明能被檢查
數學證明最難的地方，是「對不對」往往得靠人一行行讀、花上幾天甚至幾年才能確認。OpenAI 這次的另一個重點，是把許多證明的形式化版本一併放上，用的語言叫 Lean。
Lean 是一種程式語言，專門用來讓數學證明「被電腦檢查」。你把證明寫成 Lean 的形式，電腦就能一步步驗證每個推論合不合法，不合就報錯。這種機器可檢查的特性，理論上讓證明比純文字手稿更容易被獨立核實。
OpenAI 在聲明裡也講清楚了分工：他們協助準備手稿、把證明形式化，並對正確性負責；但數學論證本身，是由系統生成的。換句話說，人類的角色偏向整理與形式化，核心的推理來自模型。
OpenAI 這批數學結果為什麼引來震動
把 722 篇放進學術界此刻的氣氛裡，才能理解為什麼震動。過去一年，AI 在數學競賽與部分研究問題上的表現屢屢超出預期，數學圈對「AI 到底能推進多少真正的開放問題」本來就處於高度緊繃的狀態。這次一次湧進數百篇，等於往這個已經在震盪的領域再丟一顆石頭。
OpenAI 的野心不只於此。有報導提到，他們同時分享了一份 AI 生成的 Navier–Stokes 千禧年難題解答，附帶 Lean 證明。千禧年大獎難題是數學界公認最硬的一批問題，任何一篇相關成果都會被放大檢視。
問題出在核驗。多家媒體指出，這批手稿的核驗程度參差不齊，OpenAI 並未對外做獨立的 Lean 執行驗證。也就是說，形式化證明雖然「可以被機器檢查」，但這次沒有人公開把整批拿去完整跑一遍。找到證明的工具和證明真的站得住，是兩件不同的事。
另外，那座倉庫裡的東西處在不同驗證階段，而產出它們的模型又沒有對外釋出，外界要複製或查核並不容易。
這批手稿對數學研究意味著什麼
對數學研究者，這批材料是一份值得逐篇檢視的線索庫，而不是可以直接引用的定論。Lean 形式化的部分相對可靠，因為機器能查；純手稿的部分，仍需要同行評審。把它當成「值得看的候選結果」比當成「已被證實的定理」更恰當。
為什麼 Lean 這麼關鍵？因為它把「對不對」從人的閱讀，變成機器可以重跑一次的工序。
對一般讀者，重點不在你是否看得懂證明，而在方向：AI 正從「解題」往「做研究」推進。這件事會改變接下來幾年學術界的工作方式：人類數學家可能花更多時間在審核與整理 AI 產出的結果，而不是從零推導。
接下來值得關注的，是社群有沒有開始獨立跑那批 Lean 證明，以及是否會出現第一批被第三方確認或駁倒的結果。在那之前，OpenAI 這 722 篇更像一份大膽的公開宣告，而不是已經蓋章的成果。
