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

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

• Bend：用证明阻断AI错误的编程语言2026-09-17
• 社区推出oai-math-revised，修订OpenAI数学文稿2026-10-24
• HN讨论：数学家为何抛弃OpenAI2026-10-17
• 陶哲轩回应OpenAI数学成果发布2026-10-08
• AI辅助完成11个正方形最优堆叠证明2026-10-07