菲尔兹奖得主陶哲轩12年前的预言，AI帮他实现了

这件事是什么？跟普通人有什么关系？

全球最聪明的人之一、菲尔兹奖得主陶哲轩，12年前在颁奖台上说过一句话：未来数学家写论文，可能不再用LaTeX（一种排版工具），而是用计算机能懂的语言。当时听起来像天方夜谭，因为那时候连ChatGPT的影子都没有。但过去这一年，AI在数学领域突然加速，陶哲轩亲自带队，用AI和人类协作的方式，48小时内就攻克了2200万个数学问题中的大部分。这告诉我们：AI不只是聊天机器人，它正在帮科学家快速验证数学猜想，未来可能加速新发现，甚至影响你用的密码学、天气预报背后的算法。

陶哲轩是谁？

陶哲轩是数学界的天才：2岁教大孩子数数，7岁学微积分，10岁成为国际数学奥赛最年轻的奖牌得主，31岁拿下数学最高奖菲尔兹奖。但他不喜欢单打独斗。他一直想：数学家能不能像程序员一样，在网络上合作解题？一个人知道A，另一个人知道B，合起来会不会发现新东西？

从协作到自动化验证

2009年，他参与了一个叫Polymath的项目，让数学家们在网上一起解决难题。效果不错，但问题来了：人越多，检查错误越费劲。没有自动工具，验证速度跟不上协作规模。

2014年，他预言了三个方向：

• 大规模数学协作会成为常态
• 计算机能自动验证数学证明
• 论文会被机器能读懂的语言代替

当时没人当回事。但后来，一个叫Lean的工具出现了。

Lean是什么？

Lean是一套交互式定理证明系统。简单说：你把数学证明写成代码，Lean会逐行检查逻辑是否正确。就像一个超级严格的老师，每步都要证明“为什么这里等于那里”。

陶哲轩亲自下场

2023年，48岁的陶哲轩决定学习Lean。他挑了一道不算难的题，心想一周就能搞定。结果发现：写数学论文和写形式化证明完全不是一回事。在论文里，一句“三个大于1的数相加大于等于3”没人会质疑，但Lean要求你明确每个引理来自哪里。最后他花了一个月才完成。但从此，他成了形式化数学社区的一员。

三周完成，48小时攻克大部分

2023年底，他和合作者写了一篇关于PFR猜想的论文（一个关于数字集合加法结构的难题）。论文写完，他立刻在Lean社区发起项目，把论文拆成小任务，开放给全球志愿者。每个人完成一块，Lean自动验证。结果三周全部完成！

2024年9月，他发起更大的项目：研究约2200万个代数等式之间的关系。他用了新方法——AI帮写证明，Lean检查，全球志愿者分工。48小时内，大部分问题就被解决。第9天进度达99.866%，第57天基本完工。这个项目还催生了数学新概念“原群上同调”（一种研究代数结构的理论，可以想象成给数学结构拍X光片）。

结论：最好的预言是亲手实现

陶哲轩用行动证明：不止是预言未来，而是亲手把未来造出来。现在他成了AI数学最坚定的推广者，建议年轻学者学会和AI协作。普通人也可以期待：未来AI能帮科学家更快破解难题，推动技术进步。