Terence Tao 博客详解 Lean 定理证明器可靠性与 AI 关联

Terence Tao 博客刊发 Thomas Hales 客座文章《数学家应该了解的 Lean 定理证明器：可靠性问题与 AI》，聚焦形式化证明与 AI 的关联。文章指出目前并不知道 Lean4 是否一致、也不清楚为何应当一致，且所有已知的一致性证明策略都存在真实障碍。文章还讨论了形式化证明对数学可靠性的意义。