Anthropic 用 Claude 跑通了费马大定理的形式化证明。

耗时与规模：人类数学家当年写了129页。AI 只用了11天，敲出1300万行代码。它顺手证明了近3万条中间定理。这体量是最大数学定理库的5倍多。

怎么做到的：靠几十个 AI 智能体互相协作。清华姚班毕业的彭天翼带队。他开发了 Prove2Me 平台当“项目经理”。这工具给 AI 派活、管记忆，才没让它们翻车。

到底证明了啥：不是重新发现新解法。而是把怀尔斯当年的证明翻译给机器查。Lean 编译器全跑通了，说明绝对严谨。

对数学界意味着啥：以后顶级证明都能这么验错。普通人花几天账号费，也能验证复杂定理。不过 AI 只是当裁判，离自己创定理还远。