陶哲轩在“害怕”什么？

📋总体概括

菲尔兹奖得主陶哲轩于10月9日在博客转发数学家托马斯·黑尔斯的文章《数学家应该了解的Lean定理证明器：可靠性与人工智能问题》，直指AI数学浪潮的核心矛盾：AI正以前所未有的速度攻克过去数学家需耗时数年甚至数十年才能完成的证明难题，如OpenAI于10月6日在GitHub上发布的相关成果，但AI批量生产数学证明的可靠性如何验证，成为人类必须直面的信任问题。Lean形式化证明系统正是为此而生的验证工具，其与AI的关系成为数学界热议焦点。