Claude用11天完成费马大定理形式化证明，写下1300万行Lean代码

会懂网AI资讯，9月8日，Anthropic公布，Claude用11天完成费马大定理的形式化证明，这是首个可由计算机完整检查的端到端证明。项目写下约1300万行Lean代码，规模超过Mathlib五倍。

费马大定理由安德鲁·怀尔斯在1994年证明，是人类数学史上的里程碑。但怀尔斯的原始证明长达上百页，依赖大量未被形式化验证的推理步骤；将其转化为计算机可逐行检查的形式化证明，是一项浩大工程。

Lean是一种交互式定理证明器，可以把数学命题与证明过程编码为计算机可验证的形式。它的特点是每一步都必须严格符合逻辑规则，无法通过”显然可得”来跳过，这使得验证的可靠性达到最高级别。

项目由数十个智能体并行推进，消耗约60亿输出Token，产出30300个可验证定理，其中29500个进入最终证明，且仅使用Lean的三条公理。仅用三条公理完成如此规模的工作，说明证明的构造极为严谨。

这一成果的意义不仅在数学本身，更在于验证了AI在超长程推理任务上的能力。形式化证明需要极强的逻辑一致性——任何一处细微错误都会导致后续全部失效，能够完成如此规模的自我一致推理，说明模型的长程规划能力有了实质提升。

当然，也有人提出质疑：形式化证明本质上是把已有数学成果翻译成机器语言，AI的角色更接近”翻译者”而非”发现者”。但无论如何，1300万行可验证代码的产出，本身就是对AI工程能力的一次极限测试。

从方法论看，这一成果也推动了”AI辅助形式化”的研究热潮。数学界长期希望建立可机器验证的证明库，但人工形式化的成本过高。若AI能把这一成本降低一个数量级，形式化验证有望成为数学研究的常规环节。