Claude 11 天完成费马大定理的机器证明

Formalizing Fermat's Last Theorem

Anthropic 团队宣布，Claude 在 11 天内自主完成了费马大定理（Fermat's Last Theorem）的首个完整计算机验证证明。这项任务此前被数学家预计需要数年，而 Claude 通过编写 1300 万行 Lean 代码，证明了 29500 个中间定理，最终在 Prove2Me 平台的协作下成功闭环。Kevin Buzzard 评价这一成就标志着数学自动形式化的重大突破，未来 AI 将能大幅减轻人类验证数学证明的负担，并帮助建立更可靠的数学知识体系。