ChatGPT三个月内连干翻三个百年数学猜想，人类数学家是不是该收拾东西回家种地了？
AI工具在2026年夏天狂飙突进，从推翻厄尔多斯单位距离猜想，到解决格罗滕迪克60年群论难题，再到反杀雅可比猜想，数学家们从震惊到麻木只用了三周。大语言模型加定理证明器这套组合拳，正在把数学发现变成流水线作业，而你还在用手算微积分？
反例轰炸机已经起飞，人类还在停机坪上发呆
2026年5月20号，ChatGPT直接把厄尔多斯单位距离猜想给毙了。这个猜想在离散几何领域蹲了几十年，结果AI说这玩意儿是错的，还顺手扔出来一个反例。更狠的是，它用的还是1960年代高洛德和沙法列维奇搞的深奥数论定理，直接把人家几十年前的老古董翻出来当武器用。
你以为这就完了？图样图森破。OpenAI那边刚宣布完，逻辑智能公司立马跟进，说他们的系统已经把AI生成的论文自动形式化成Lean代码了。换句话说，AI不光会猜，还会写证明，而且写的是机器能查的那种。你还在纠结ε-δ语言呢，人家已经在跑百万行代码的证明了。
我认识的那些数学家，刚开始还端着架子说“我不信”，结果没几天全真香了。原因很简单，当AI能在三周内生成一百二十万行Lean代码，而人类九年才憋出两百三十万行的时候，你再端着那就是跟自己过不去。Lean这东西说白了就是个定理证明器，能让机器帮你检查数学证明有没有漏洞，以前是人类给机器上课，现在是机器给人类上课。
数论大炮打蚊子，但蚊子真的死了
仔细扒一下这个厄尔多斯反例，你会发现它特别狡猾。它不跟你正面硬刚几何问题，而是绕了个大弯子，用类域论这种数论核弹来炸。问题是类域论那玩意儿证明起来得要一百多页纸，全是上世纪初期攒下来的老古董，到现在都没人能把它压缩成短证明。
我学生谢爱迪生搞的博士课题就是形式化局部类域论，干了一年才快收工。全球类域论？那玩意儿在2025年的时候看着还像科幻小说。结果2026年6月26号，OpenAI的鲍里斯用新模型Sol直接把整个反例给完全形式化了，啥额外假设都没用，就从数学公理开始硬推。
你说气不气人？人学生吭哧吭哧读博搞的东西，AI三周给你干完了，还附赠一百多万行验证代码。这就像你花了十年练成一门绝技，结果人家上来就掏出一把加特林。但话说回来，AI生成的代码不能直接信，因为Lean本身是个编程语言，恶意代码能删你硬盘。所以我第一件事就是放沙箱里跑，确认它只是在证明数论上同调定理，不是要格式化我的电脑。
群论老问题被秒，人类专家开始否认三连
格罗滕迪克那个问题就更有意思了。这老哥六十年前问了个事儿：每个n阶有限自由群概形是不是都会被n杀死？说白了就是问一个代数结构能不能被自己的阶数整除。德尔尼证了交换情况，格罗滕迪克自己证了基约化情况，舒夫又往前推了一大步，去年还有人发论文继续推进。
结果AI进场之后，七天之内就扔出来一个4阶群概形不被4杀死的反例。文件只有1076行，我五分钟就编译完了，确认它确实在说“这里有个反例”，而且证明能跑通。然后我让阿希尔把代码提交到mathlib库里，这事儿就算结了。
但真正精彩的不是反例本身，而是人类专家的反应。我同事在午餐时说“这问题这么容易就被解决，说明人类根本没花时间认真想”。我没好意思告诉他，我早年曾经花了一整周死磕这个问题。他这状态明显就是悲伤五阶段里的否认期，后面还有愤怒、讨价还价、抑郁，最后才能到接受。AI都骑脸输出了，有些人还在嘴硬说“这问题不重要”，问题是那问题搁那儿六十年了，你怎么没去解决呢？
更扎心的是，我学生安德鲁用AI工具两周写了二十五万行Lean代码，把一个模性提升定理给完全形式化了。这玩意儿对我证明费马大定理至关重要，结果AI两周干完的活儿，搁以前得是博士后干两年的量。然后我还收到同事邮件，说研究生每月花两百刀买AI工具简直是疯了。我回他说，现在哪个博士生不买这玩意儿才是真疯了。
雅可比猜想被干翻，人类正式进入围观模式
重头戏是雅可比猜想。这玩意儿在代数几何里挂了整整一百年，无数人往里填过坑。结果2026年世界杯决赛那天，AI悄咪咪地把它解决了。当然，解决的方式是找到了反例，所以严格来说是把猜想给毙了。
莱文特在推特上宣布这事儿的时候，我第一反应是“又来？”阿希尔还问我“要不要再提交个PR？”结果这次他慢了半拍，保罗已经手动形式化了反例，先一步提交到了DeepMind的形式化猜想仓库。这个仓库牛在哪儿呢？它把一堆数学猜想提前用Lean语言精确表述好了。所以AI只要产出一个能编译通过的证明文件，机器就能自动验证这个反例成不成立。整个过程不需要人类数学家再看那些又臭又长的证明细节，机器全包了。
所以现在的流程变成了这样：人类先把猜想翻译成机器语言，AI负责找反例或者证明，机器自动检查对错，最后人类负责理解和解释。人类在数学发现里的角色，从运动员变成了裁判，再到现在的解说员。你说这是进步还是退步？我觉得是进步，因为解说员不用在场上跑得气喘吁吁，还能看得更清楚。
数学家在震惊中走向麻木，反例多到不值钱了
整个六月到七月，我被反例轰炸到麻木。先是厄尔多斯，再是格罗滕迪克，然后是雅可比。每个反例单独拎出来都够发一篇顶级期刊，结果它们在三周内扎堆出现，搞得跟菜市场大甩卖一样。
最讽刺的是什么？是这些反例的难度排序完全反着来。厄尔多斯那个最难，一百多万行代码，用了全球类域论这种核武器。格罗滕迪克那个中等，一千多行。雅可比那个反而相对简单，但因为被提前形式化好了，验证起来最方便。人类花了六十年、一百年搞不定的东西，AI像拔钉子一样一个个拔掉。你说人类数学家现在是什么心情？反正我认识的那几个菲尔兹奖得主，嘴上说着“AI只是工具”，眼神里已经写满了“我是不是该转行了”。
但我觉得吧，这事儿没那么悲观。AI找反例确实猛，但它不太擅长解释“为什么这个反例重要”。阿希尔现在就在死磕格罗滕迪克反例的深层结构，不是满足于“这里有个反例”，而是想搞清楚“这个反例揭示了什么本质”。这种洞察力，这种把具体反例升华成一般理论的能力，目前AI还不太行。至于以后行不行，那就看下一波更新了。
反正我现在的心态就是，别跟AI比速度，比深度。你跑得再快也跑不过汽车，但你可以当那个开车的人。
作者：Kevin Buzzard，伦敦帝国理工学院数学教授，Xena项目发起人