Claude 用 11 天跑完费马大定理：不是证明了数学，是验证了数学

Anthropic 放出个挺炸裂的成果：用 Claude 在 11 天里，完成了费马大定理首个机器验证的 Lean 形式化证明。

先说清楚，这事儿容易被人喊大，但也容易被人误读。我尽量把它讲准。

它到底干了什么

费马大定理本身，是 1994 年就被人严格证明过的东西，不是新闻。真正的新闻是：Claude 把这个人类已经写出来的证明，翻译成了一种机器能逐行核验的形式语言（Lean），而且从开头到结尾跑通了，机器确认无误。

打个比方：定理是人类早就证出来的，Claude 干的是把那本厚厚的证明手册，重新抄写成一份"计算机能逐句挑错"的版本，并保证每一环都对得上。这活儿如果交给人类形式化团队，往往要好几年；Claude 11 天干完了。

形式化验证一直是数学和工程里的"苦活"。一个证明哪怕人觉得没问题，要变成机器能验证的严密链条，中间有大量机械、繁琐、极容易出错的转写。过去这是少数专家才能啃的硬骨头，进度慢得让人着急。

Claude 把这道门槛削平了一大截。意义不在于"AI 发现了新数学"，而在于"AI 让已有的数学变得可被机器信任"。这对科研是个底层基建的升级——以后重要结论出来，可以更快地被形式化、被核验，而不是躺在论文里等人慢慢审。

别把它理解成"AI 自己想出了费马大定理"。它验证的是已知结果，不是新定理。距离 AI 独立提出并证明一个人类没想到的真命题，还差得远。

而且 11 天这个数字，依赖的是人类几百年积攒下来的证明思路当底子。没有那个底子，模型连从哪下手都不知道。

这件事真正的价值，是给科研装上了一套"自动审稿机"。它不会改变谁提出定理，但会改变定理被信任的速度。

往后搞研究的，手里会多一件趁手的兵器：你证完，AI 帮你把证明焊死成机器可验证的版本。至于"AI 自己搞数学"那天什么时候来，这次的成果说明我们在路上，但远没到。