數學界正討論 OpenAI 近日公開的 719 篇 AI 生成數學手稿是否值得信賴。原因是有新論文指出，該公司早前高調宣稱已證明的 Navier-Stokes 證明，其書面版本與電腦形式化驗證（Lean 程式碼）並不吻合。
要點整理：
- OpenAI 最初公布 722 篇手稿，其後因一個符號正負號出錯，撤回 3 篇，現餘 719 篇。
- 三名英國數學家指出，Navier-Stokes 書面證明與 Lean 程式碼有兩處明顯不一致。
- 作者沒有指證明錯誤，但重申電腦驗證不能取代傳統同行評審。
OpenAI 數學成果釋出惹關注
OpenAI 於 10 月 6 日一次過上載數百篇 AI 生成數學手稿。其後有報道在周四刊出，指稱這批工作未有完全遵守一個由獨立數學家小組為 AI 實驗室所訂下的業界指引。該批手稿原有 722 篇，OpenAI 其後在翌日於官方資料庫中 撤回 3 篇，原因是一項證明中的正負號出錯，連帶依賴該結果的另外兩篇亦須下架。
該套指引由 9 名成員組成的 「數學與人工智能諮詢小組」（Advisory Group on Mathematics and Artificial Intelligence） 於 9 月 29 日 發表，開宗明義便要求實驗室停止以封閉專有模型，去「測試」高階數學難題。OpenAI 的資料庫則聲稱，這批手稿是來自一個未公開的內部模型，對開放數學研究問題進行嘗試所得。
在所有結果之中，只有 10 篇附有模型推理的文字摘要；約 42% 的主要結論已用 Lean 形式化，讓電腦逐步核查證明是否邏輯完備。
延伸閱讀： Anthropic 行政總裁人工幾多？IPO 文件有披露
Navier-Stokes 證明出現落差
來自倫敦國王學院的 Alexander Bastounis，以及劍橋大學的 Fabian Circelli 和 Anders Hansen，近期在預印本平台發表論文，詳細檢視 OpenAI 於 9 月宣布攻克的 Navier-Stokes 證明。
三人指出，OpenAI 公開的書面證明與 Lean 程式碼至少有兩處不符，其中一處尤為關鍵：程式碼實際上只證明了一個較「弱」的估計，而非論文正文聲稱的較「強」結論。
作者強調，他們沒有判斷書面證明本身是對是錯，而是提出一個更細緻的問題：Lean 只告訴大家，最終定理在形式系統內是「站得住腳」，卻無法保證人類讀到的每一步推理都與程式碼一一對應。換言之，即使有形式化驗證，這類工作仍然需要傳統的同行評審，逐行審查人類版本的證明。
菲爾茲獎得主 陶哲軒（Terence Tao） 在 10 月 6 日於社交平台 撰文 指出，目前不少難題其實是由「AI 提示工程師」（AI prompters）推動解決，但這些人未必真正理解輸出內容，難以在研討會中解說，或在面對深入提問時作出合理回應。
哈佛大學教授、諮詢小組成員 Melanie Matchett Wood 亦表示，當這些 AI 生成結果一公開時，「其實沒有任何一位人類真正理解全部細節」，真正的工作反而是「由那一刻才正式開始」。
OpenAI 證明風波延燒
該諮詢小組早前已表示，最終只有更廣泛的數學社群，才有資格判斷 OpenAI 在多大程度上遵守了其建議。這場審視來得並不意外，因為過去一個月爭議不斷。
OpenAI 於 9 月 8 日高調宣布攻克 Navier-Stokes 方程的一個核心問題，隨即與紐約大學數學家 Tristan Buckmaster 爆出學術貢獻歸屬爭議。其後三日，25 位菲爾茲獎得主聯署發表聲明，警告若任由大規模 AI 產出未經充分審查的數學結果，可能對整個學科帶來長遠傷害。
在這場風波下，如今再被揭發書面證明與形式化程式碼有落差，難免進一步動搖市場與學界對 OpenAI 數學成果的信心。
