人工智能时代的数学

有时候，一本书恰好迎合了它的时代。出版行业很有趣——研究、写作和编辑一个故事需要数年时间，而它出版时的世界往往与最初签约时大不相同。2020年，凯文·哈特内特报道了IMO大挑战，这是一项早期尝试，使用当时鲜为人知的程序Lean来训练AI参加国际数学奥林匹克竞赛。此后几年，我们见证了机器辅助数学的爆发式发展。2026年5月底，OpenAI的一个模型推翻了埃尔德什著名的单位距离问题，该问题已悬而未决80年。两星期后发布的《莱顿宣言》已有超过2000名数学家签署，成为数学界如何看待AI的现状声明。

正是在这场变革中，凯文的书《代码中的证明》问世了。突然之间（令人高兴地！），每个人都想谈论数学、计算机和AI。凯文出现在《纽约时报》科技播客Hard Fork上讨论莱顿宣言，在《Quanta Podcast》上概述从黑板到计算机化数学的巨大转变，并在《Breaking Math Podcast》上谈论他的著作、Lean进入主流的过程，以及“Lean与我们当前AI时刻的完美融合”。

《Breaking Math》联合主持人Noah Giansiracusa称其为“多年来我读过的最好的数学书——最接近捕捉詹姆斯·格雷克的《混沌》魔力的作品。一部真正的数学惊悚片！”（在此订购《代码中的证明》。）

在这些虚拟对话中，凯文与出版商托马斯·林在西蒙斯基金会进行了一场公开对话，题为“构建真理机器”。面对满座的观众，凯文分享了他多年来跟踪Lean发展的轶事，以及与当今塑造数学和AI的关键人物的对话。他指出，这两个话题现在密不可分：“模型通过强化学习变得好多了。要这样做，你需要一个环境来提供尖锐的反馈信号。通过Lean，你可以让模型做数学题，用Lean代码输出答案，并获得即时反馈……这就是大实验室关心的原因……它完全处于AI模型训练生态系统的核心。”

两人讨论了在一个AI可能成为数学家的有用工具或不可思议的替代者的世界中解决问题的未来。凯文对人机合作的未来持乐观态度，但他也向学生提出建议：“你需要学习数学。你需要以一直以来学习数学的方式学习它，理解概念，并与之斗争。如果你想像陶哲轩那样指挥AI，你需要那种深层次的理解。”（你可以在这篇文章顶部的视频中观看完整对话。）

即将举行的活动

7月底，与作者凯文·哈特内特和陶哲轩以及Quanta Books团队在费城宾夕法尼亚会议中心举行的国际数学家大会（ICM）见面。这是世界上最大的数学会议，每四年举办一次，自1986年以来首次在美国举行。参观Quanta Books展位#102，我们将出售《代码中的证明》，并抽取Quanta Books手提袋、T恤和陶哲轩的《六项数学基础》的早期样书。

7月25日星期六，上午11:00至中午12:00 签名书板：陶哲轩 地点：展位#102（E厅） 陶哲轩将为他即将于10月27日出版、现已开放预购的《六项数学基础》签署书板。他对数字、代数、几何、概率、分析和动力学这六个核心数学概念的简洁而优雅的巡览，“精美地提炼了数学的本质……只有像他那样知识渊博的人才能做到”，3Blue1Brown的格兰特·桑德森如是说。对于我们的世界杯球迷，数学作家本·奥尔林称赞阅读《六项数学基础》“就像通过梅西的眼睛看足球”。

7月25日星期六，下午1:15至2:15 《代码中的证明》：凯文·哈特内特与托马斯·林的对话 地点：本杰明·霍尔舞台（E厅） 凯文·哈特内特将与托马斯·林讨论《代码中的证明》。随后，他将在Quanta Books展位（#102）签署他的书。

您可以在官方网站上注册ICM，或注册免费的公共数学节活动，例如凯文于7月25日星期六的活动，以及陶哲轩于7月24日星期五的ICM公开讲座。

希望在那见到您！