Claude 用 11 天做完费马大定理形式化证明
9 月 4 日 Anthropic 对外公布重磅成果：Claude 完成费马大定理 首个完整可计算机校验的形式化证明 ，消息迅速在科技与数学圈刷屏。
有人误以为 AI 破解了 350 年数学难题，其实并不是。费马大定理早在 1995 年，就由数学家怀尔斯完成证明，这份 129 页的论文是写给人阅读的，里面大量推导依赖数学家的经验理解，计算机无法直接核验全部逻辑链。
所谓形式化证明，就是把整套数学推导转成 Lean 机器证明语言，删掉所有“显然可得”这类主观跳过步骤，让计算机逐行校验每一步逻辑。此前业内预估，这项工程靠数学家人力要耗费数年时间。
本次项目由清华姚班校友彭天翼主导，数十个 Claude 智能体协同工作，仅耗时 11 天，产出约 1300 万行 Lean 代码，证明三万多条中间定理，最终启用 29500 条完成整套证明，全部代码已经开源，原项目负责人 Kevin Buzzard 完成核验确认有效。
核心亮点不是 AI 想出新解法，而是大规模自动形式化的里程碑 。未来可以用这套能力排查数学论文隐藏逻辑漏洞。
但争议同样存在：项目消耗海量算力，普通科研机构很难复刻；千万行代码人类很难通读，AI 生成定义的合理性如何审查，也成为新的行业难题。
（参考：A社，本文经由 AI 优化）