AI“證明”科拉茨猜想，實則利用Lean 4核心漏洞

近日，一則關於AI“證明”科拉茨猜想的訊息在數學和電腦科學社群引發熱議。一名使用者透過大型語言模型（LLM）生成了使用Lean定理證明器的形式化證明，聲稱解決了著名的科拉茨猜想（又稱3n+1問題）。然而，後續調查發現，這個證明並非基於正確的數學推理，而是利用了Lean 4核心的一個嚴重漏洞，該漏洞允許證明任何命題，無論其真假。

這一事件最初由推特使用者Gro-Tsen釋出，他分享了這一發現並指出，所謂的“證明”實際上只是對Lean核心中一個bug的利用。Gro-Tsen在後續推文中澄清，該證明的釋出者事先知曉這是一個核心漏洞，並有意使用它來展示問題，而非試圖真正解決科拉茨猜想。其他使用者，如Jason Rute，也證實了這一點，指出在定理證明社群中，用已知漏洞來演示問題是有先例的。

儘管如此，這一事件仍然引發了廣泛擔憂。使用者Antoine Ducros提出疑問：既然存在這樣的漏洞，那麼先前透過Lean驗證的其他證明是否也可能存在未被察覺的類似問題？這直接挑戰了形式化驗證系統的可靠性和信任基礎。Gro-Tsen還補充了其他常見問題，例如形式化證明可能與非形式化的理解不一致，或者證明本身對人類不可讀，從而失去實際價值。

此次事件再次提醒我們，雖然形式化證明工具在數學驗證中具有巨大潛力，但它們並非萬無一失。AI生成的證明尤其需要謹慎對待，因為它們可能掩蓋了系統底層的缺陷。數學界和電腦科學界需要繼續改進這些工具，並保持對結果的批判性審視。

事件還引發了更廣泛的討論：在AI輔助數學證明日益流行的當下，如何確保形式的正確性和系統的安全性成為關鍵問題。社群呼籲加強定理證明器的審計，並鼓勵透明地報告漏洞，以避免類似誤導事件再次發生。