陶哲轩在“害怕”什么？

📋总体概括

10月9日，菲尔兹奖得主陶哲轩在其博客转发了数学家托马斯·黑尔斯的文章《数学家应该了解的Lean定理证明器：可靠性与人工智能问题》，聚焦AI批量生产数学证明背景下的可靠性问题。文章指出当前AI数学浪潮的核心矛盾：AI正以前所未有的速度攻克过去需数学家耗费数年甚至数十年才能完成的证明难题，但人类凭什么确信这些证明可靠？ Lean等形式化验证工具成为讨论焦点，OpenAI此前也于10月6日在GitHub上发布了相关成果，引发学界对AI数学可信度的深层思考。