《陶哲轩为何成为 AI 数学布道者》

导语

这篇 Quanta 长文写陶哲轩如何从世界级数学家变成 AI 与证明助手的积极推动者。它的重点不是“AI 会不会替代数学家”，而是数学研究正在出现一种新形态：人类提出方向、把问题拆解，机器和社区一起验证越来越多细节。

1. 陶哲轩关心的是人机协作，而不是自动取代

文章把陶哲轩放在一个转折点上：他并不把 AI 看成能立刻解决所有数学难题的神奇机器，也不把它当成威胁数学家的竞争者。他看重的是 AI、形式化证明和协作平台结合后，能改变数学家组织工作的方式。

这种改变尤其体现在证明助手 Lean 上。Lean 要求数学命题被写成机器可检查的形式，每一步都必须严谨。它会拖慢随手推导，却能让复杂证明被拆分、复查和长期维护。数学从“少数人读懂一篇证明”，开始走向“很多人和机器共同维护一个可验证对象”。

2. 从 Erdős 到 Tao，数学协作本来就有传统

文章回顾陶哲轩早年作为神童进入数学共同体的经历，并提到他与 Paul Erdős 等数学家的关系。这个背景不是传记装饰，而是说明陶哲轩一直身处高度协作的数学文化中。