AI 輔助“推翻”考拉茲猜想失敗，Lean 4.32.2 修復內核漏洞

# AI 輔助「推翻」考拉茲猜想失敗：Lean 內核漏洞被發現並修復

一項曾引發廣泛關注、宣稱藉助 AI 在形式化證明系統 Lean 中「推翻」考拉茲猜想的工作，最終被證實無效。這項工作的缺陷根源並非數學推理本身的思路問題，而是所使用的 Lean 定理證明輔助系統存在一個內核漏洞。該漏洞會讓某些不正確的邏輯判斷逃過檢查，甚至可能導致系統錯誤地接受「False」命題。Lean 團隊在收到報告後迅速行動，已於 7 月 28 日發佈 4.32.2 版本修復了這一問題。考拉茲猜想是一個歷史悠久且表述極其簡單的數學難題，由德國數學家洛塔爾・考拉茲（Lothar Collatz）於 1937 年提出。

該猜想又稱奇偶歸一猜想或 3n+1 猜想，其規則非常容易理解：對於任意正整數 n，如果它是偶數，就將其除以 2；如果它是奇數，就將其乘以 3 再加 1。得到新數字後重複上述操作，理論上最終總會得到 1。例如從 6 開始，路徑為 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1。儘管無數數學家嘗試證明或證偽，這個猜想至今仍未得到解決。在此次事件中，形式化驗證專家 Ramana Kumar 於 7 月 25 日在 GitHub 上發佈了一個項目，最初聲稱藉助 AI 成功推翻了考拉茲猜想。

值得注意的是，該項目並沒有給出具體的反例整數，而是在 Lean 系統中證明了「存在一個無法到達 1 的數」。因為考拉茲猜想宣稱所有正整數最終都會到達 1，只要能證明存在某個正整數不滿足這一性質，就足以推翻整個猜想。而使用 Lean 進行形式化證明，意味著這個推理過程要經過計算機嚴格驗證，因此該聲稱一經發佈便吸引了大量關注。Lean 是一款著名的定理證明輔助系統，屬於形式化驗證工具。它允許用戶將數學命題、定義和證明過程編寫成程序代碼，然後由 Lean 的內核對這些代碼進行自動檢查，確保每一條邏輯規則都正確應用，每一個類型都匹配。

簡單來說，用戶寫出的證明必須能通過計算機的「機械檢查」，才能被認為是有效證明。這種方式能極大降低人為疏忽或複雜推理中隱含錯誤的風險，因此在數學、計算機科學以及軟硬件驗證領域都有重要應用。然而，就在 Ramana Kumar 發佈項目後不久，他在審查反駁內容的過程中發現了異常：利用某些方法，甚至能讓 Lean 無條件接受「False」這個代表假命題的邏輯值。「False」是邏輯系統中最基本的矛盾命題，如果系統可以接受 False，就意味著系統本身是不一致的——任何命題都可以被證明為真，形式化驗證的可信度將徹底崩塌。

這一發現立刻表明，該項目所謂的「證明」很可能建立在一個有缺陷的基礎之上，並不能真正說明考拉茲猜想是錯誤的。形式化驗證研究者 Kiran Gopinathan 隨後對問題進行了深入分析，並成功將其縮減為一個小型、可重現的代碼示例。他於 7 月 28 日將這一精簡後的復現代碼正式報告給 Lean 開發團隊。這個最小化案例非常關鍵，它讓開發人員能夠快速定位問題出在系統的哪個環節，而不是在一團複雜的證明代碼中大海撈針。Lean 團隊迅速介入調查，發現漏洞的根源位於內核處理「嵌套歸納類型」的部分。在類型論中，歸納類型是一種構建數學對象的方式，而嵌套歸納類型則涉及更複雜的定義結構。

問題在於，當系統處理這類類型時，有時會忽略所謂的「幽靈類型參數」——這是指那些不直接出現在數據結構組件中、但會影響類型含義的參數。簡而言之，由於沒有正確檢查這些幽靈參數，某些原本應該被判定為錯誤的參數，竟然能夠逃過驗證程序。Lean 開發者 Leonardo de Moura 對此表示，問題在於內核的實現沒有完成應有的檢查。內核是整個系統的信任基礎，一旦內核存在漏洞，任何基於它構建的形式化驗證結論都不可靠。值得注意的是，Leonardo de Moura 也是 Lean 的主要設計者之一。在收到報告約 1 小時內，Lean 團隊就創建了修復此問題的拉取請求，效率極高。

相關修復被合併後，Lean 4.32.2 版本於 7 月 28 日正式發佈，這一版本包含了對該漏洞的完整修復。此次事件對形式化驗證社區和依賴 Lean 進行數學研究的用戶群體而言，可以說是一次重要的提醒。一方面，它展示了形式化驗證系統並非萬無一失，即使是經過精心設計的內核，也可能隱藏著極其隱蔽的邏輯漏洞。另一方面，社區對待該漏洞的態度也體現了形式化驗證的價值所在：如果沒有計算機系統對證明過程進行嚴格檢查，這樣細微的錯誤恐怕很難被察覺，而正是因為 Lean 允許並鼓勵用戶審查系統行為，漏洞才得以在短時間內被發現和修復。從更宏觀的角度看，這一事件也為 AI 在數學研究中的應用提供了寶貴教訓。

近年來，AI 輔助證明已然成為一個熱門方向，大語言模型、自動推理器等工具能夠幫助數學家生成猜想、構建證明的草稿，甚至填補難以察覺的推理步驟。然而，這並不意味著 AI 的輸出可以未經驗證就直接作為數學結論。AI 可能產生看似合理但實際無效的推理，特別是在涉及複雜邏輯結構時。形式化驗證系統可以作為一道重要的安全防線，但前提是系統本身必須正確無誤。目前，考拉茲猜想依然懸而未決。本次事件沒有推翻它，也沒有提供新的有效證據，但它讓更多人認識到了形式化驗證在數學研究中的工作方式及其潛在難點。未來，隨著 AI 技術的不斷發展，AI 與形式化驗證工具的結合預計將更加緊密。

如何在充分發揮 AI 強大搜索與生成能力的同時，確保最終結論經過可靠驗證，將是數學與計算機科學交叉領域需要持續探索的課題。而這次 Lean 內核漏洞的及時修復，無疑為這項事業提供了一次珍貴的實戰經驗。