堪薩斯大學教授24小時剔除OpenAI攻破Connes猜想證明中的漏洞
為何重要
這個案例揭示了 AI 在繁瑣的數學形式化工作中具備效率，但在嚴謹的數學定義對齊上仍無法取代直觀的人類審查。對於依賴形式化工具的開發者而言，將「假設驗證」與「邏輯驗證」分開處理是必要的風險控管手段，否則可能產生經核心驗證通過的錯誤結果。
OpenAI 宣稱其新一代模型解決了 Connes 剛性猜想等難題，堪薩斯大學教授 J. L. Nielsen 在 24 小時內指出其形式化證明存在關鍵漏洞。
- Nielsen 分析了 OpenAI 公開的 37000 行 Lean 4 程式碼，發現其中一個群未滿足 ICC 或 Kazhdan 性質(T) 等必要附加條件。
- 程式碼中的引理處理物件可能經過對偶變換，導致與原群定義的介面無法正確對接，使得證明與猜想的關係失效。
- 這說明瞭形式驗證工具（如 Lean）雖能保證邏輯的嚴謹性，但無法替代人類對「猜測前提」是否被正確表達的審查。