數學界近日對 OpenAI 公開的 719 篇 AI 生成數學手稿是否可信，提出嚴厲質疑。原因是一篇新論文指出，OpenAI 早前公布的 Navier-Stokes 證明，其書面版本與經電腦形式檢查的 Lean 程式碼存在出入。
重點整理：
- OpenAI 最初聲稱有 722 篇手稿，其後因一個符號（正負號）錯誤牽連三篇論文，被迫撤回，庫存減至 719 篇。
- 三名英國數學家指出，OpenAI 的 Navier-Stokes 書面證明與 Lean 程式碼有兩處出現分歧。
- 作者未斷言證明錯誤，但強調「機器檢查」不能取代傳統同行評審。
OpenAI 大規模數學放料
OpenAI 於 10 月 6 日一次過上載大批數學手稿。周四公布的一份報告 指出，相關做法偏離了由獨立數學家小組為 AI 實驗室訂立的指引。該數學庫最初共有 722 篇手稿，OpenAI 其後在翌日 撤回 3 篇，原因是一處正負號出錯推翻了一個關鍵論證，連帶倚賴該結果的另外兩篇亦受影響。
上述指引由一個九人組成的 數學與人工智能諮詢小組於 9 月 29 日 發布，開宗明義呼籲各大實驗室，勿再以專有閉源模型解高深數學難題作「壓力測試」。OpenAI 在其資料庫說明中則表示，這批論文來自一個尚未公開的內部模型，針對開放研究問題所作的演算。
現時只有 10 個結果附有模型推理過程的文字摘要，而整體約 42% 的「主結果」已用 Lean 形式化——Lean 是一種可由電腦逐步檢查證明是否嚴謹的程式語言。
延伸閱讀：Anthropic 行政總裁實際賺幾多？招股書有答案
Navier-Stokes 證明現「斷層」
來自倫敦國王學院的 Alexander Bastounis，以及劍橋大學的 Fabian Circelli 與 Anders Hansen，近日 重審 OpenAI 在 9 月高調公布的 Navier-Stokes 證明。他們發現，書面論文與 Lean 程式碼至少有兩處不一致，其中一處更涉及估計強度：程式碼實際證明的只是比論文聲稱更「弱」的估界。
三人刻意避談該書面證明最終對錯，立場相對克制；他們的核心論點是：Lean 雖可確認最後定理本身「站得住腳」，但無法保證人類在紙本上閱讀到的所有中間步驟同樣嚴謹，故此即使有機器形式檢查，相關工作仍離不開傳統同行評審。
菲爾茲獎得主 陶哲軒（Terence Tao） 亦在 10 月 6 日於社交平台 撰文 指出，目前不少難題是由「AI 提示工程師」解出，但這些操作者本身並未真正理解輸出的數學內容，以致無法就結果接受質詢或作學術報告。哈佛教授、同為諮詢小組成員的 Melanie Matchett Wood 則形容，這些結果在發布當下，根本「沒有任何一個人真正完全理解」，真正的工作是「由現在才開始」。
OpenAI 證明爭議升溫
諮詢小組早前已表明，只有更廣泛的數學界才能評斷 OpenAI 在多大程度上遵守了他們的建議。如今新一輪審視，正好延續近月緊張氣氛。
OpenAI 於 9 月 8 日宣布取得 Navier-Stokes 突破，其後立即與紐約大學數學家 Tristan Buckmaster 差點鬧出「搶功」風波；再過三日，25 名菲爾茲獎得主聯署發表聲明，警告大量「工廠式」AI 數學產出，可能對學科生態造成損害。
