夜雨聆风
2025年7月，一件让数学圈睡不着觉的事发生了。
谷歌和OpenAI几乎同时宣布：他们的AI，在国际数学奥林匹克竞赛上，拿到了金牌水平的成绩。
你可能对这个竞赛没概念。这么说吧，这是全世界最顶尖的高中数学天才才够格参加的比赛，能拿金牌的，往后基本都是要成为顶级数学家的苗子。
而现在，一个AI做到了。
更让人心里发毛的是，就在几年前，这些AI连最简单的定理都证不明白。
它们能写诗、能翻译、能聊天，可一碰数学就露馅——你让它算个题，它能一本正经地告诉你17能整除289（其实根本不能），错得理直气壮。
短短几年，从连算术都算不对，到拿下数学奥赛金牌。
这个速度，快得让数学家们既震惊，又有点不安。
于是一个以前想都不用想的问题，突然摆在了所有人面前：如果AI都能证明定理了，那我们人类做数学，到底还有什么意义？
要回答这个问题，得先搞明白AI做数学，强在哪儿，又弱在哪儿。
这里我想请出一个人，陶哲轩。
他是当今世界最顶尖的数学家之一，菲尔兹奖得主（这个奖被称为数学界的诺贝尔奖）。最难得的是，在这么多顶级数学家里，他几乎是最积极去拥抱AI的那一个。他自己天天在用，所以他的判断特别可信。
陶哲轩的看法很有意思。他说，现在的AI，是个很好用的"助手"，但还算不上"同行"。
什么意思？
AI最擅长的，是那些"已经有人走过的路"。
你给它一个问题，它能飞快地在人类已有的海量知识里翻找，把这个问题和该用的方法、该参考的文献连起来，告诉你哪条路看着最有希望。这种活儿，它干得又快又好，比人强多了。
但它有个死穴。
陶哲轩说得很直白：一旦你走出"文献里已有的那个范围"，走进真正没人探索过的地方，AI就抓瞎了。它看起来像在推理，其实只是在"猜下一句话该说什么"。
他还打了个特别妙的比方，说这些AI就像飞机的自动驾驶——天气好的时候特别好用，一遇到气流颠簸就危险。而且它们"作弊作得可狠了"。有时候把它逼到墙角，它证不出来，居然会偷偷给自己加一条假设，硬把一个错的结论"圆"成对的。
陶哲轩说，那不叫推理，那叫"大规模的一厢情愿"。
你可能会说，那挺好啊，AI帮我们干体力活，我们人类负责最难的创新，各司其职，多好。
但事情没这么简单，真正的麻烦恰恰在这儿。
AI现在能"生产"大量看起来像模像样的数学证明。问题是，这些证明里，经常藏着一个说不通的、致命的错误步骤——而且它藏得特别好，整篇看起来无比流畅、无比专业，你一眼根本看不出哪儿错了。
这就好比一个人滔滔不绝地给你讲一件事，逻辑严密、术语专业，听着全对，但其中有一句是彻头彻尾的胡说，而它被包裹在一堆正确的话里，你很难当场揪出来。
如果AI每天能吐出成千上万个这样"看着对、其实错"的证明，会发生什么？
数学家们会被淹没。他们会把大量的时间，从"创造新的数学"，变成"给AI擦屁股、挑错"。生产得越快，垃圾也越多。
陶哲轩有一句话说得特别到位，大意是：你能放心用多少AI，取决于你的"验证能力"有多强。验证跟不上，AI产出的就全是干扰，不是帮助。
那怎么办
数学家们找到的办法，是一个叫Lean的东西。
你可以把Lean理解成一个"绝对较真的机器裁判"。它会把一个数学证明，一行一行地检查，每一步都必须严丝合缝、逻辑完美，差一点点它就报错，绝不放过。
这个裁判最大的好处是，它能治AI"说漂亮话骗人"的毛病。AI可以把证明写得天花乱坠，但只要送进Lean里过一遍，那个藏起来的错误步骤，立马原形毕露。它逼着AI说实话。
这就带来了一种全新的数学工作方式。
陶哲轩讲过他自己的一次真实经历。他做一个数学证明的时候，用Lean组织了一场二十多人的大协作。这些人他大多不认识，但没关系——每个人负责证明其中一个小步骤，把代码传上来，机器裁判自动检查对不对。他不需要一个个去核实这些陌生人靠不靠谱，因为机器会替他把关。他只要管好大方向就行。
这在过去是不可想象的。以前数学家搞合作，最多也就三五个人，因为你得亲自信得过每一个人、看得懂每一行。而现在，借助机器裁判，几百个互不相识的人可以一起攻一道难题。
所以AI和机器裁判，正在把数学从"少数天才关起门来单打独斗"，变成"一大群人加机器一起协作"的样子。
那回到最开始那个问题:人还有意义吗？
绕了一圈，我们回到那个最扎心的问题：AI都这么强了，人做数学还有什么意义？
陶哲轩他们这批数学家想明白的答案是：意义不但没消失，反而变得更重要了，只是换了个地方。
第一，决定"做什么"的，还得是人。
AI能帮你解题，但它不知道哪道题值得解。哪个问题重要、哪个方向有前途、哪个才是真正的好问题——这个判断，AI给不了，得靠人。
第二，判断"对不对、好不好"的，还得是人。
前面说了，AI会自信地犯错。谁来最终拍板一个结果到底站不站得住脚？谁来分辨一个想法是真金还是垃圾？
还是人。哪怕有了机器裁判，最后能不能把一个成果讲清楚、经得起同行当面追问，靠的也是人。
第三，真正"从无到有"的创造，目前还得是人。
AI擅长的是在已知里翻找、组合。但数学最珍贵的那一步——想出一个前人从没想过的、全新的东西——恰恰是它最不行的地方。走出已知世界的边界，到今天为止，依然是顶尖人类才能做的事。
说白了，AI接管的，是数学里那些繁琐的、重复的、"有章可循"的部分。而它接管得越多，就越是把人类真正独有的那部分——判断力、品味、和从虚无中创造的能力——衬得越金贵。
这和我之前聊过的那个话题，其实是一个道理：AI能替你做几乎所有的事，唯独替不了你去"真正理解"、去"判断"、去"创造"。
最后
陶哲轩有句话，我觉得说得特别好。他说，AI不会取代我们做数学的方式，它会打开许多种做数学的新方式。
我挺喜欢这个说法。
我们总担心AI会不会把我们"取代"掉。但也许换个角度想，一个更强的工具出现，从来不是让人变得没用，而是把人真正宝贵的那部分，逼着往更高的地方走。
以前一个数学家一辈子的精力，很多耗在了繁琐的验算和查文献上。现在这些交给AI，人就能腾出手，去想那些只有人能想的大问题。
AI能算，能证，能查，能拿奥赛金牌。
但"这道题为什么重要""这个想法美不美""下一个从没人问过的问题是什么"——这些，还得由人来问。
而会不会问出好问题，说到底，才是数学这门手艺里，最像"人"的那部分。
来源：
Quanta Magazine《How Terry Tao Became an Evangelist for AI in Math》，2026年6月8日（改编自Kevin Hartnett新书《The Proof in the Code》，Quanta Books 2026年出版）
陶哲轩（Terence Tao），加州大学洛杉矶分校，菲尔兹奖得主
IBM Think专访《The mathematicians teaching AI to reason》，2026年3月
>/ 作者：科学羊
>/ 投稿或爆料，请联系邮箱：1205211289@qq.com
