AI 證明懸置 18 年開放問題，Lean 驗證鏈受審視

據 DEV Community 11 月 7 日釋出的一篇文章，本週一個 AI 研究系統證明了量子複雜性理論中懸置 18 年的開放問題，並且證明帶有一份完整的 Lean 形式化，已被 Lean kernel 接受。文章指出，以往 AI 生成的證明通過形式驗證器時，人們的第一反應是問數學是否正確，但現在這已不是唯一的問題。

一個 kernel 驗證過的證明，其可信度取決於它所依賴的系統、定義、庫和工具鏈，因此驗證環節本身同樣需要接受審計。截至該文釋出，被證明的具體問題名稱、AI 系統的身份，以及該形式化在 Lean kernel 中的具體接受情況，都未在現有材料中給出。