數學家24小時駁回OpenAI攻破的猜想！“AI證對了每句話，但已跟原猜想無關”

OpenAI近日宣稱新一代AI模型一口氣破解十個世界級數學難題，其中一項是推翻Connes剛性猜想。這項宣稱很快遭遇人類數學家的正面反擊——隔天就有一篇論文回應指出，AI提出的反例其實並不成立。撰寫回應論文的學者，是堪薩斯大學拓撲物理中心的J.L.Nielsen。他花了整整一天的時間，把OpenAI公開的37000行Lean 4代碼從頭到尾追了一遍，把每一個數學對象逐一對回它們的原始定義，最終找出兩條互相獨立的失敗路徑。整個事件的關鍵不在AI證得對不對，而是AI從一開始就搞錯了「要證什麼」。所謂Connes剛性猜想，是法國數學家Connes在1980年前後提出的命題。

數學上可以替一個群配上代數結構，有時兩個表面上看起來不同的群，配出來的結構卻完全相同。Connes猜測，只要群滿足兩個附加條件，這種混淆就不會發生：結構一樣，群就必須一樣。這兩個條件分別叫做ICC與Kazhdan性質(T)。因此，想反駁這個猜想，必須找出兩個滿足上述條件的群，它們彼此不同構，卻能生成相同的代數。OpenAI新模型的做法正是如此：構造出兩個不同構的群，讓它們生成同一個代數，並附上證明，宣稱兩個群都滿足ICC和性質(T)。整套論證寫成37000行Lean 4代碼，由Lean內核逐條驗證通過，另外還附了一份說明文檔，解釋這兩個群是如何搭建起來的。

Nielsen的質疑點非常明確：AI構造的其中一個群，其實並沒有滿足附加條件，既不是ICC，也沒有性質(T)。也就是說，整個反例從前提就不成立。他進一步指出，這個錯誤可能來自三種情況：代碼中的性質(T)沒有忠實對應Kazhdan的原始定義；或者證明只對部分對象成立，卻被套用到了整個群上；又或者代碼裡的那個群，根本不是說明文檔中所描述的那個群。為了把話說死，Nielsen做了一件極其費力的事。OpenAI公開發布的是整合成單一文件的代碼，早期分模組的源碼結構已經消失，所有原本的名稱都無法直接對應。

他於是自行列出一張對照表，把每個數學對象在新代碼中的名稱與行號一一標出：零上閉鏈群在第13700行，扭曲群在第14069行，兩套代數同構的證明在第36712行，主定理則在第36954行。針對ICC的部分，Nielsen也把整條推理鏈追了一遍。這條鏈從第31430行開始，一層一層往上傳遞，最後在第31610行合成結論。他指出的問題在於，這些引理處理的是經過對偶變換之後的對象，並非原本那個帶中心元素的群，因此根本沒有直接覆蓋關鍵的元素區域。至於這些引理是否對最終進入定理的那個具體群中的每一個元素都成立，取決於兩塊構造之間的接口如何對接。換句話說，問題出在「要證什麼」，而不是「證得對不對」。

Lean只負責驗證後者，對於前者一無所知。至於另一個扭曲的群，Nielsen態度相對保留。他說自己沒有從代碼中獨立核實它到底滿不滿足ICC，也承認代碼裡的引理有可能確實證明了它滿足。但這不影響最終結論，因為其中一個條件已經確認不成立，整個反例就站不住腳。他也把自己的兩條反駁意見寫成了Lean代碼，並且在Lean 4.32.2版本下成功編譯。把這件事放大來看，暴露的是形式驗證工具的本質限制。Lean內核能保證的，只是一段證明在形式上嚴絲合縫，卻不負責這個證明是否真的對應原初的數學猜想。

陶哲軒先前就曾警告過：驗證證明的是形式陳述本身，而不是這個陳述與使用者意圖是否相符，因此人類的審查無法直接被機器取代。這類事故在學界已有前例。一份針對五個常用Lean基準的審計，就找出了4833條問題，包括反例、空洞定理與不可靠公理，而且這些問題全都通過了機器驗證。最後是人類數學家親自構造出反例，才發現被證明的那句話本身是錯的。統計學習理論的形式化工作中，最危險的情況被描述為「不是一個失敗的證明，而是一個對錯誤陳述的成功證明」。張量網絡方面的研究也記錄過類似現象：系統給出的證明形式上完全正確，只是它證的那個命題比預期要弱得多。

Nielsen在論文結尾寫道，OpenAI那份形式化可能把它聲稱的每一條結論都建立對了，但Lean內核檢查不了的，是這些結論與猜想原話之間究竟有沒有關係。人類閱讀猜想時會注意到前提條件，而證明助手拿到一個不滿足前提的結論，照樣會驗證關於這個結論的任何斷言。截至目前，Connes剛性猜想仍然處於開放狀態。