我们分享了费马大定理的第一个完整的计算机验证证明。Claude在11天内基本自主地使用Lean编程语言编写了该证明。下面，我们描述形式化是如何完成的，并分享一些关于这项工作对研究数学可能意味着什么的思考。

大约在1637年，皮埃尔·德·费马在他所著的丢番图《算术》一书的页边空白处写下了一个断言，这个断言后来成为有史以来最著名的数学猜想之一：对于任何n > 2，不存在正整数a、b、c满足aⁿ + bⁿ = cⁿ。费马大定理（FLT）后来被证明极其难以证明。第一个证明由安德鲁·怀尔斯爵士于1995年提出，长达129页，并花费了数月艰苦的验证工作。

十年后，荷兰计算机科学家扬·贝格斯特拉提出了“形式化”怀尔斯证明的想法：将数学推理转换为计算机可以自动检查的形式。从那时起，数学家们一直在开发编码如此复杂证明所需的方法，包括2024年由伦敦帝国理工学院的凯文·巴扎德发起的多年社区努力，旨在使用Lean证明助手完成形式化。

最近，Anthropic研究员田一鹏（其哥伦比亚大学团队构建AI形式化工具）开始测试Claude是否能在形式化FLT方面取得进展。结果超出了他的预期。在11天内，Claude基本自主地生成了FLT的第一个端到端、计算机验证的证明。在此过程中，它编写了1300万行Lean代码，并证明了29,500个中间定理。