陶哲轩的AI实验：数学是如何从“孤岛艺术”变成“大科学”的

顶尖数学家陶哲轩最近成了AI和Lean（定理证明器）的布道者，有人觉得他被大厂收买了，有人觉得这毁掉了数学的美感。但真正有意思的不是他怎么用AI，而是他想解决什么。

陶哲轩一直想推行“大规模协作数学”，以前卡在“人肉验算”的信任瓶颈上。现在，他通过Lean把数学定理代码化，用AI去跑繁琐的证明微步骤，最后由机器自动验证。这套组合拳把复杂的数学问题拆解成几万个简单子问题，让AI和志愿者并行解决。

这给我们的启发是，AI最大的颠覆性不在于“生成”，而在于把协作和验证的信任成本降到了零。数学正在告别传统的“孤岛天才”模式，向现代物理学那种成百上千人协作的“实验科学”演进。这才是知识生产方式的范式转移。

www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/