1300万行Lean代码：Claude用11天把费马大定理形式化了

哥伦比亚大学商学院助理教授彭天翼用Claude做了件挺硬的事：11天，完成了费马大定理的第一个完整的、经计算机检验的形式化证明。

规模：1300万行Lean代码，途中证明了29500个中间定理。

形式化证明和”AI证明了定理”不是一回事。费马大定理1994年就被怀尔斯证明了，形式化要做的是把那套横跨多个数学分支的论证，一行一行翻译成机器能逐步检验的代码，中间不允许有”显然”和”类似可得”。这活儿以前是几十人几年的量级——Lean社区做费马大定理的官方项目原计划就是多年工程。

关键不在模型本身，在流程。他们用的是一个叫Prove2Me的平台，把定理陈述组织成无环图，多个智能体按图协作。这解决的是长链推导里最要命的问题：单个智能体在几千步之后会开始重复劳动、跑偏、互相推翻，最后耗光资源什么也没证出来。

把依赖关系画成图之后，每个智能体只负责图上的一小块，验证器保证接口对得上。

这件事的实际价值可能不在数学本身，而在审稿。现在一篇复杂论文的正确性靠几个同行读几个月，读漏了就漏了。如果形式化的成本能降到”一个人加十来天”，那么”这个证明对不对”就变成了一个可以跑出来的结果。