數學界正重新檢視 OpenAI 釋出的 719 篇 AI 生成數學手稿是否值得信任。起因是一篇新論文指出， 該公司先前大肆宣傳的 Navier-Stokes 證明， 其論文文字版內容與經電腦形式化驗證的 Lean 程式碼並不完全相符。
重點整理：
- OpenAI 最初公布 722 篇手稿，但因發現一處符號正負號錯誤，連帶影響兩篇依賴該結果的文章， 隨後火速下架 3 篇，庫存降至 719 篇。
- 英國三位數學家記錄到，OpenAI Navier–Stokes 證明在兩個關鍵位置上， 論文文字敘述與 Lean 程式碼推導出現分歧。
- 作者並未直接宣稱證明錯誤，而是強調：機器形式驗證只能檢查定理是否被「某種形式」證明， 但無法取代人類對論證細節的同儕審查。
OpenAI 數學手稿釋出風波
OpenAI 於 10 月 6 日公開這批數學手稿；周四發布的一篇報導則指出， OpenAI 的做法與一個由數學家組成的獨立小組，先前為 AI 實驗室擬定的指引存在落差 （報導見：分析）。
這批資料庫最初包含 722 篇手稿。隔日，OpenAI 在其 GitHub 儲存庫中宣布 撤回 3 篇論文： 其中一篇因符號正負號錯誤導致論證崩壞，另外兩篇則依賴於該錯誤結果，只能一併撤出。
相關行為準則由九人組成的 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 方程證明。他們指出，該成果的論文版與 Lean 程式碼至少在兩個地方不一致， 其中一次分歧，是程式碼實際證得的估計明顯「較弱」，並未達到論文文字聲稱的強度。
作者們刻意不對「論文證明本身是否正確」下定論。他們的論點更為精細： Lean 程式碼能確認最終定理確實被證成，但並不能保證， 論文中人類可閱讀的中間推理步驟都嚴謹無誤。因此，即便有形式化驗證背書， 這類 AI 協助完成的證明仍然必須接受傳統的同儕審查流程。
費爾茲獎得主 陶哲軒（Terence Tao） 也於 10 月 6 日在 貼文中提到， 目前有許多難題看似被所謂的「AI prompters」解出，但這些操作者本身並不真正理解輸出內容， 無法在研討會上完整回答問題或清楚報告其工作。身為該顧問小組成員的哈佛大學教授 Melanie Matchett Wood 則表示，當這些結果發布時，「沒有任何人真正理解它們， 接下來才是工作真正開始的時候。」
OpenAI 證明可信度之爭
顧問小組先前已表態，究竟 OpenAI 在多大程度上遵守其建議， 應由更廣泛的數學社群來評判。這番審視，緊接著的是一個緊繃的月份。
OpenAI 於 9 月 8 日高調宣布解決 Navier–Stokes 難題，隨即與紐約大學數學家 Tristan Buckmaster 爆發功勞歸屬爭議；三天後，包括 25 位費爾茲獎得主在內的學者， 聯合發表聲明，警告大量、快速生產的 AI 數學成果，恐怕會損害整個領域的健康發展。
