Lean 修補核心 soundness 漏洞 #14576：AI 輔助產生的 Collatz 猜想錯誤反證曾獲接受

依這份尚無其他來源佐證的事後報告，Lean 核心的 soundness 漏洞 #14576，曾讓一份由 AI 輔助產生、不含 sorry 的 Collatz 猜想錯誤反證通過檢查；漏洞於 7 月 28 日通報後一小時完成修補，隨後經審查合併，新版修補程式已發布。 Ramana Kumar 於 7 月 25 日公開該反證的程式碼庫。Kiran Gopinathan 於 7 月 28 日將問題縮減為一份簡短的 False 證明並建立 #14576；修補 PR #14577 由 Joachim Breitner 審查及提出改進建議。 問題出在核心處理巢狀歸納型別：當歸納型別 T 的參數 Ds 是未出現在建構子欄位中的 phantom parameters，這些參數會從產生的輔助型別消失並逃過型別檢查，使核心可能以型別錯誤的引數接受 False 證明。漏洞只能透過 metaprogramming，將歸納宣告直接送入核心觸發；Lean 前端原本就會檢查引數並攔下錯誤項，因此報告將其定性為實作錯誤，而非 Lean 後設理論的缺口。 原始 Collatz 程式碼庫也通過一週前版本的 nanoda。nanoda 是 Chris Bailey 以 Rust 實作的獨立 Lean 核心，但它另有一項未驗證投影節點型別名稱的漏洞；Jeremy Chen 通報並在 Lean 漏洞曝光前一週修補。該證明利用兩個彼此無關的錯誤，讓官方核心未檢查的運算式同時被舊版 nanoda 接受。Kumar 認為時間重疊可能只是巧合，但無法排除模型曾看過 nanoda 的漏洞通報；Breitner 則提出，強大模型已能尋找這類漏洞，可能是時序巧合的原因。 報告認為，獨立核心交叉檢查仍然有效，因為這次利用鏈需要兩套實作各自存在不同漏洞，但使用者必須同步採用兩者的最新版本。lean4lean 也受官方核心漏洞影響，原因是其歸納型別處理移植自參考實作；該專案對 Lean 型別理論與核心實作的驗證仍在進行，一致性證明尚未涵蓋歸納型別。 Lean FRO 已把這項利用方式，以及 Arthur Adjedj 提出的相關非一致參數案例加入 Kernel Arena 迴歸測試。後續 PR #14582 改為檢查巢狀出現位置的參數是否確實具有參數行為，而非僅重新進行型別檢查。 OpenAI 的 Daniel Selsam 另以專攻資安的 AI 協助 Lean FRO，找到多項只能透過 metaprogramming 觸發的核心程式錯誤；這些問題均已修補，且全部能被 nanoda 攔截，相關 PR 為 #14607、#14608、#14609、#14613、#14615、#14616。團隊也透過 #14621、#14631、#14632 強化核心不變量；comparator.live 現在預設執行 nanoda，並每日追蹤其上游版本，讓 lean-eval 與 comparator 在修補後保持更新。 針對限制或移除 metaprogramming 的建議，報告指出 Lean 的 elaborator 原本就是不受信任元件；攻擊者仍可直接製作 .olean 檔案或修改記憶體繞過 elaborator，因此核心必須在自身程序內拒絕型別錯誤的宣告。