Thomas Hales 系统梳理 AI 时代 Lean 的可信边界：kernel check 之外仍需 statement fidelity 与独立交叉验证

Thomas Hales 10 月 9 日在 Terence Tao 博客发表长文，系统解释 Lean proof 的 elaboration / kernel trust model，并强调“kernel 接受”不能自动证明形式陈述忠实表达原数学问题：AI 时代还必须审计 definitions、theorem statement、未经授权公理与 informal-to-formal correspondence。文章回顾 2026 年 Lean soundness bugs、AI 辅助发现 kernel / elaborator 问题的案例，讨论 Comparator、独立 kernels 与 Con-Leche 等交叉检查路线；Hales 同时指出，在其判断下截至 2026 年 10 月仍缺少覆盖 Lean abstract type theory 的完整公开 relative-consistency proof，并主张 foundational trust claims 需要比单个 kernel run 更强的公开证据。