數學界正質疑 OpenAI 公布的 719 篇 AI 生成數學稿件是否足以信賴。最新研究指出，該公司先前聲稱已證明的 Navier-Stokes 方程證明 與其在電腦上形式驗證的版本並不相符。
重點摘要：
- OpenAI 公開的數學稿件，從原先 722 篇縮減為 719 篇，原因是公司因號誌（正負號）錯誤撤下 3 篇論文。
- 三名英國數學家記錄到兩處文字版 Navier-Stokes 證明與其 Lean 程式碼不一致。
- 作者並未指稱證明錯誤，但強調機器檢驗無法取代傳統的同儕審查。
OpenAI 數學成果釋出爭議
OpenAI 於 10 月 6 日公布這批 AI 生成數學稿件集，而在週四出爐的一份報告中，有學者檢視後指出，OpenAI 的作法偏離了一個由獨立數學家小組替 AI 實驗室制定的指導方針。這份論文集上線時共有 722 篇稿件，OpenAI 隔天即在其版本歷史中宣布撤回 3 篇：一篇因號誌錯誤導致其中一個論證失效，另兩篇則建立在該錯誤論證之上。
這套指導原則由「數學與人工智慧諮詢小組」（Advisory Group on Mathematics and Artificial Intelligence）於 9 月 29 日發布，開宗明義就要求各實驗室停止在封閉的專有模型上測試高階數學難題。OpenAI 在其開源庫中則表示，這批論文來自一款尚未對外釋出的內部模型，該模型被拿來挑戰開放的前沿研究問題。
依 OpenAI 自行公開的說明，目前只有 10 則結果附上模型推理過程的文字摘要；另外約 42% 的「主結果」被形式化寫入 Lean —— 一種讓電腦能逐步檢查數學證明正確性的程式語言。
延伸閱讀：Anthropic 執行長薪資多少？IPO 文件揭露答案
Navier-Stokes 證明的落差
來自倫敦國王學院的 Alexander Bastounis，以及劍橋大學的 Fabian Circelli 與 Anders Hansen，近期在論文中詳查 OpenAI 9 月宣布完成的 Navier-Stokes 方程證明。他們指出，文字版證明與 Lean 形式化程式碼至少在兩處出現分歧，其中一處是程式碼實際證得的估計，比論文聲稱的結論明顯「較弱」。
作者強調，他們並未宣稱文字版證明必然錯誤，而是要凸顯一個更細緻的問題：Lean 的形式驗證可以確定最終定理是否成立，但無法保證人類實際閱讀的中間推導步驟都合乎嚴謹要求。因此，這類「機器驗證」成果仍然需要傳統的同儕審查程序。
費爾茲獎得主 陶哲軒 於 10 月 6 日在社群平台上撰文指出，目前有不少難題實際上是由「AI 提示工程師」解出，但這些操作者本身對產出內容的理解有限，往往無法在研討會中清楚回答問題或進行完整報告。作為諮詢小組成員的哈佛教授 Melanie Matchett Wood 則表示，這類結果在發布之際，基本上「沒有任何人真正理解」，真正的學術工作其實是從那一刻才開始。
圍繞 OpenAI 證明的更大爭議
該諮詢小組已表明，只有更廣泛的國際數學社群，才有資格評估 OpenAI 在多大程度上遵循了其建議。如今的嚴格檢視，緊接著的是過去一個月的緊張局勢。
OpenAI 於 9 月 8 日宣布 Navier-Stokes 方程的突破性結果，隨即與紐約大學數學家 Tristan Buckmaster 爆發學術貢獻歸屬爭議。僅僅三天之後，25 位費爾茲獎得主聯名發表聲明，警告大規模生產式的 AI 數學成果可能傷害整個領域的健康發展。
