数学家Hales撰文讨论Lean形式化数学的可靠性。2026年AI自动形式化取得突破，Fermat大定理等被快速形式化，但同年夏季发现多个Lean内核可靠性漏洞，可证明假命题。应对方案包括多内核交叉验证、形式化验证内核（如Con-Leche）及加强类型论元理论研究。作者警告AI时代不可盲信系统，需人类审计。