昨晚临睡前刷到一条消息，困意直接没了：Claude用11天，把费马大定理的证明"翻译"成了计算机能逐行检查的版本，代码量1300万行。

先给不熟的朋友补个背景。费马大定理是17世纪一个法国数学家写在书边上的猜想，大意是：n大于2时，两个数的n次方相加，不可能等于第三个数的n次方。他当年还留了句名言——"我想到了一个绝妙的证明，可惜空白太小写不下"。这一"写不下"就是350多年，直到1995年才被英国数学家怀尔斯攻克，而且他第一版证明还查出有漏洞，又补了一年才过关。

这里有个外行很难体会的差距：人脑看数学论文，很多地方一句"这里显然成立"就跳过去了，但计算机不吃这套，每一步都得从最基础的规则推出来，错一个符号都不行。所以把费马大定理的证明"翻译"给计算机，数学界本来是当多年工程来规划的——帝国理工的团队2024年才正式启动，光技术蓝图就写了86页。

结果Claude一来，11天干完了。更离谱的是，带队的Anthropic研究员彭天翼（清华姚班毕业、MIT博士）最初只想测测AI能把这事推多远，压根没想干这么大，结果几十个AI分身并行开工，有的补定义、有的攻中间定理、有的负责拼装，最后堆出3万多个中间定理，人类只在旁边偶尔指点一句"这个方向优先"。

这事跟普通人有什么关系？关系还真不小。以前"机器验证数学证明"靠人一行行搬，慢如蜗牛，所以绝大多数数学论文从没被计算机验证过。现在最难啃的骨头之一被AI啃下来了，等于给数学界打通了一条流水线——以后不管是新出的证明，还是几百年前没人验过的旧证明，都可能被AI快速搬进计算机过一遍。数学家那句"我觉得我证对了"，终于有了个不近人情的裁判来较真。

我的看法可能和替数学家焦虑的人不一样。这次Claude干的是"搬运"和"翻译"，不是发现新证明，真正的创造还在人手里。但它把数学家从最枯燥、最耗人力的活里解放了出来——以后人只管想，琐碎验证交给AI。我尤其欣赏Anthropic那句表态：AI说自己证完了不算数，必须让程序逐行检查通过才算。这种"自己说了不算、机器点头才算"的较真劲儿，才是AI最该被普及的态度。AI开源技术的未来发展趋势是什么
费马大定理