数学家安德鲁·怀尔斯在1995年发表费马大定理证明时，那篇论文有129页。
为了验证这129页纸，顶尖人类大脑们熬了几个月。
现在，Anthropic的Claude只花了11天。
11天，1300万行Lean代码，29500个中间定理。
老实讲，看到这个数据的时候，我第一反应是这模型是不是在胡乱凑字数。但帝国理工的数学大佬Kevin Buzzard看完后直接盖章：这是历史性的自动形式化成就。
书页边缘的装X笔记，坑了人类三个半世纪
先给不熟悉数学史的朋友补个课。
1637年，皮埃尔·德·费马在书页空白处写了个猜想，还极其嚣张地留了句话：我找到了一个绝妙的证明，但空白处太小写不下。
就这一句话，把后世数学家折磨了350多年。
1908年有人悬赏10万德国金马克，放今天大概一两百万美元，结果第一年就被薅了621个错误证明。
直到1993年怀尔斯站出来，讲了三天课，结果两个月后被人揪出致命漏洞。他又苦熬了一年才把坑填上。
人类证明数学定理，本质上是在拼逻辑链条。
只要断了一环，后面全废。人类写论文还喜欢跳步，那些显而易见的步骤直接就省了。
但计算机不吃这一套。
要想让Lean这种证明助手验证，你得把每一个极其微小的步骤都喂给它。帝国理工的团队今年刚启动费马大定理的形式化项目，光是初期蓝图就写了86页，大家估摸着这活儿得干好几年。
几十个AI智能体疯狂内卷，中途还翻过车
哥伦比亚大学的研究员Tianyi Peng想看看Claude能不能啃下这块硬骨头。
结果远超预期，不过过程并不是一帆风顺。
一开始，Claude的几个智能体很快就迷失了方向，协作彻底崩盘。
说实话，这太像我们平时在公司开小组会了，聊着聊着就不知道在干嘛。
这些翻车的废代码，大概占了最终证明里7%的非样板代码。
后来团队换了个思路，用上了开源协作平台Prove2Me。
这下场面控制住了。几十个Claude智能体开始疯狂协作，定义概念、证明中间定理、再拿去攻克更难的命题。
人类在这个过程中干了啥？
基本就是偶尔发几句高层指令，比如“雅可比作为概形听起来优先级很高”、“赶紧把Mazur定理推完”。
然后AI就自己闷头干。
当证明跑通的那一刻，Claude的内部日志里甚至能看出一种激动的情绪：
🏁🏁🏁FLT根节点在prove2me上显示PROVED。这是本次活动的最终目标。
烧掉30万美金，就为了当个超级验钞机？
有意思的是，这次AI并没有像之前搞黎曼猜想那样，弄出什么全新的数学发现。
它做的是验证。
把数学证明变成像计算器算数一样绝对可靠的验证。
有网友在评论区算了笔账：消耗了大约60亿输出token，按照API价格算，这一波大概烧掉了30万美金。
花30万美金验证一个人类早就证明过的定理，图啥？
个人觉得，Kevin Buzzard说到了点子上。
现在AI生成的数学证明越来越多，人类审稿人根本看不过来。让AI去形式化验证AI生成的数学，这可能是数学界唯一能跟上AI产出速度的办法。
这其实是在给AI自己擦屁股。
而且这技术还在下沉。Anthropic拿三个普通的Claude Max个人订阅账号，只花了3天就把Vinogradov的三素数定理给形式化了。
这意味着以后普通研究员买个订阅，也能搞这种大型验证。
数学家的饭碗保住了，但工作方式得变
很多人担心AI会抢了纯数学家的饭碗。
老实讲，机器验证永远替代不了人类能看懂的数学推导。
你让一个数学家去读1300万行Lean代码，他大概率会当场辞职。
但未来的数学论文，大概率会标配一份形式化代码。
就像现在写代码必须带单元测试一样，以后搞数学研究，不带个机器验证过的证明，你可能都不好意思投顶会。
费马大定理的证明，凝聚了三百年来无数天才的心血。从Frey到Serre，从Ribet到Mazur。现在AI用11天时间，把这些人类智慧结晶翻译成了一种机器能绝对信任的语言。
当机器开始接管验证这种苦力活，人类数学家是不是终于可以把精力全放在提出好问题上了？
又或者，当AI连验证都能做得这么完美时，它离自己提出那个绝妙的证明，还剩多远？
【锐评】：花30万刀让AI把350年前的装X笔记翻译成1300万行代码，人类数学家以后发论文怕是得先过一遍机器查重了。
参考链接：
https://www.anthropic.com/research/formalizing-fermats-last-theorem