Thomas Hales

Thomas Hales谈Lean定理证明器的可靠性与AI

数学家Thomas Hales在Terence Tao博客发表客座文章，讨论Lean等证明助手在数学可靠性方面的价值与AI相关隐忧。文章提到四色定理、Feit-Thompson定理、开普勒猜想及今年完成的球填充、Navier-Stokes爆破和费马大定理等重大形式化项目，使形式化验证获得更广泛关注。