Claude用11天完成费马大定理形式化证明，代码达1300万行
AI 首次将费马大定理这类世纪难题完整转为机器可验证的证明，展示自动形式化数学走向工程化的可能。
Anthropic 称其 AI 模型 Claude 在 11 天内完成了费马大定理的完整形式化证明，即把已有证明转写为计算机可逐行核验的 Lean 代码。整个工程约 1300 万行，证明 3 万多个定理，过程中人类只给出少量方向性提示。
正文摘录
.jpg) 费马大定理，终于有了一份能由计算机从头检查到尾的完整证明。 就在刚刚，Anthropic 声称，Claude 在 11 天内完成整个工程，写下约 1300 万行 Lean 代码，过程中人类只提供了少量高层指导。  完整的证明请参见 GitHub：https://github.com/anthropics/fermats-last-theorem 这次 Claude 没有提出新的证明路线，它所做的是把已有证明转写成机器能够逐步核验的形式，让每一个逻辑环节都接受计算机检查。 对于费马大定理这样的世纪难题，此前数学界普遍预计，完整的形式化工程需要数年时间。 为什么费马大定理还要再「证明」一次？ 1637 年前后，法国数学家皮埃尔・德・费马在《算术》一书的页边写下一个判断：当整数 n 大于 2 时，不存在满足 aⁿ+bⁿ=cⁿ的正整数 a、b、c。 他还留下一句：自己已经找到了一个「绝妙的证明」，只是页边太窄，写不下。 此后的 350 多年里，一代代数学家不断尝试。1993 年，安德鲁・怀尔斯在三场讲座中公布证明。两个月后，审稿人发现其中存在关键缺口。怀尔斯与理查德・泰勒又花费近一年完成修补，最终于 1995 年发表长达 129 页的完整证明。 费马大定理从此有了公认答案，但验证大型数学证明仍高度依赖人类。 数学论文通常会省略显而易见的步骤，也会直接调用前人已经建立的结论。