昨天一口氣放出 722 篇 AI 數學手稿的 OpenAI，剛剛撤回了其中 3 篇。
原因說來簡單：一個正負號寫錯了。
剛剛，OpenAI 在 openai/math 倉庫中發布了第一份更新日誌。日誌顯示，OpenAI 撤回 3 篇手稿，修訂 14 篇，另有 13 篇更新了引用。倉庫裡的手稿總數從 722 篇降為 719 篇。
一個正負號，拖垮三篇論文
被撤回的三篇論文，都和千禧年大獎難題之一的霍奇猜想有關：
Algebraicity of Weil classes on split abelian eightfolds
Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
The rational Hodge conjecture for products of K3 surfaces
問題出在第一篇。OpenAI 在撤稿說明中寫道，這篇論文在一處關鍵論證中把一類幾何操作的符號記成了 +1，而按論文自己的約定，它應當是 -1。
https://github.com/openai/math/blob/main/history.md
一正一負，結果天差地別。原本應該相互抵消、最終歸零的計數，變成了一個不為零的數。論文所依賴的一個經典定理，前提條件恰恰是這個計數必須為零。前提不成立，後面的整套構造隨之失去支撐。
另外兩篇論文都借用了這套構造，於是被一併撤回。
不過，OpenAI 在三份撤稿說明裡都強調了同一句話：撤回的是證明，並不意味著這些數學命題本身是錯的。原稿也沒有刪除，仍可通過歸檔連結查看。
這三篇論文都屬於倉庫第 032 號成果族，也就是此前最受關注的霍奇猜想相關成果。
撤稿之後，這一族的名字也變了：從「所有射影 K3 曲面的霍奇與 Kuga–Satake 結果」，改成了「CM 阿貝爾簇的有理霍奇猜想」。
換句話說，關於 K3 曲面的那部分結論已經從清單上撤下。這一族的核心結論，即對所有複 CM 阿貝爾簇證明有理霍奇猜想，目前仍然保留，該論文的新版本只更新了引用。
值得一提的是，出錯的那篇論文落款日期是 9 月 18 日，是倉庫裡最早的一批手稿之一。從落款到公開相隔近三週，公開後一兩天內就被撤回。至於錯誤是誰發現的，OpenAI 沒有說明。
還有 14 篇被修訂
撤稿之外，OpenAI 還修訂了 14 篇手稿，內容包括修補證明、更正結論表述、釐清前提和依賴關係。
這 14 篇涉及統計物理中的 Lipschitz 高度與 Ashkin–Teller 模型（4 篇）、複幾何中的 Kähler 極小模型綱領與豐富性（6 篇）、辛幾何（2 篇）、Navier-Stokes 流體通用計算（1 篇），以及一篇刪去過時引用的 BSD 公式論文。
其中一處修訂頗有代表性。第 342 號成果族聲稱證明了 Simon Donaldson 提出的「馴服推出相容」猜想。主結論沒有變，而且有 Lean 形式化。但論文中一個更強的附帶結論被發現說得太滿：修訂版把它收窄到特定情形，還補了一個在一般情況下不成立的例子。
形式化率：42%
更新中還新增了 6 項 Lean 形式化和 5 項輔助結果補充。按 OpenAI 的口徑，目前已有 300 篇手稿的主結果完成形式化，佔全部 719 篇的約 42%。
新增的形式化裡有幾項分量不輕，比如理論計算機方向聲稱證明對數空間計算可以完全去隨機化（L = RL = BPL）的第 103 號成果族。
需要說明的是，我們此前報導的「約六成」是按成果族統計的，即一族中只要有一篇附帶形式化就計入；OpenAI 公布的 42% 按單篇主結果統計，更能反映被計算機逐行檢查過的實際比例。
出錯的地方，沒有 Lean 把關
對照倉庫目錄會發現一個規律：這次被撤回和實質修訂的內容，幾乎都落在沒有 Lean 形式化的部分。
這也印證了此前數學界的提醒：沒有經過形式化和同行評審的結果，目前只能算「聲稱」。
好在這次勘誤處理得還算規範：錯誤寫明了，依賴鏈交代了，舊版本保留可查，符合高等研究院數學與人工智能諮詢小組建議的「修改留痕」原則。
只是，700 多篇手稿才公開兩天，第一份勘誤單就來了。它大概率不會是最後一份。
本文來自微信公眾號 “機器之心”（ID：almosthuman2014），編輯：Panda
