350年没人解得开的费马大定理，AI 11天就“验明正身”了
费马大定理，讲的道理很简单：当n大于2时，aⁿ+bⁿ=cⁿ这个等式，找不到任何三个正整数能成立。
1637年，费马把这句话写在书页边的空白处，还补了一句：“我有个绝妙的证明，可惜这页边太窄，写不下。”
嗯，他压根没写出来。
这一晃，就是358年。
人类用了多久？
直到1995年，英国数学家怀尔斯才给出完整证明，129页，写得密密麻麻。
中间还有插曲：1993年他第一次公开宣布成果，两个月后就被审稿人看出有个关键缺口，又补了一年多才堵上。
1908年，德国甚至悬赏10万金马克悬赏证明，第二年就收到了621份错误证明。
AI用了多久？11天。
Anthropic（就是做Claude那家）本周宣布，Claude在11天内完成了费马大定理的完整“形式化证明”。
啥叫形式化？就是把这129页的数学推理，翻译成计算机能逐行检查的代码。每一处推导都必须跑一遍，不许跳步、不许“众所周知”。
- 1300万行Lean代码
- 30300个中间定理
- 全程烧掉约60亿token
- 人类只给了少量方向性提示
光看这些数字，很多人会说：AI把世界难题证明了。
但真正值得咀嚼的，不是“证明”，是“验证”。
费马大定理1995年就有人证完了。数学界并不缺这个答案。
缺的是“复核”。
一篇数学论文，审稿人需要逐层追查它依赖的定义、定理和推导，常常要花上几个月甚至几年。
2024年，帝国理工的Buzzard教授发起了一个社区工程，打算用Lean把费马大定理完整形式化，官方预期周期是以“年”为单位，项目资金直接排到了2029年。
结果，Claude 11天干完了。
Buzzard看完后的评价很克制：纯数学上，“这没告诉我们任何新东西”——因为定理本来就成立。
但他紧接着补了一句：这个工程说明，AI自动形式化的产物，已经可靠到可以拿去搭楼了。
真本事，藏在一次“翻车”里
这个项目一开始其实是失败的。
几十个Claude智能体同时开工，干着干着就懵了：分不清哪个命题证过了、哪个还没证，互相重复、互相矛盾，协作直接崩盘。
直到用上一个叫Prove2Me的工具——它把所有待证的定理组织成一张依赖图，每个智能体都能看到“哪些已经完成、哪些还等着被攻克”，像一张共享的任务黑板。
说白了：几十个AI同时干活，真正缺的不是算力，是“记忆”和“分工”。
这一次，是脚手架救了场。
更大的想象空间在哪？
过去，数学证明的产出速度，一直被“人审”这个瓶颈卡着。AI生成证明越来越快，可人类审稿人就那么多。
如果每份新结果都能配一份机器可核验的形式化版本，审稿人就能把精力从“逐行抠证明”，解放到“判断这思路到底有没有价值”。
论文发表前当场验明正身，不再全靠关起门来熬几个月。
下次再有人说“AI证明了XX”，先别急着震惊。真正值钱的，从来不是它说了什么，而是它能不能让每一步都经得起机器检查。
人负责想，机器负责查。这事儿，才刚刚开始。