大约1637年，费马在书页边写下了一个猜想，后来被称为费马大定理（FLT）：对任何n>2，无正整数a,b,c满足aⁿ+bⁿ=cⁿ。1995年怀尔斯给出了129页的证明。此后数学家尝试用计算机形式化这一证明。2024年，帝国理工的Kevin Buzzard发起了社区项目，使用Lean证明助手进行形式化。最近，Anthropic研究人员测试Claude能否推动这一工作。结果，Claude在11天内几乎自主产生了第一个完整的计算机可检查的FLT证明，写了1300万行Lean代码，证明了29500个中间定理。这被认为是迄今为止最大的Lean证明。

Claude的证明遵循了Darmon、Diamond和Taylor的简化版怀尔斯证明。过程中，数十个Claude智能体协作定义概念、证明中间定理。最初几次尝试失败，贡献了约7%的非样板行代码。成功的关键是使用了Prove2Me平台（由Tianyi Peng和哥伦比亚大学合作者设计），该平台维护定理的有向无环图（DAG）以帮助智能体决定下一步证明什么，并分离定理陈述和证明文件以加速Lean编译，同时保留自然语言描述便于搜索和重用。整个形式化消耗了约60亿输出tokens，使用了与Claude Fable 5.1相当的研究模型。最终的证明被Lean检查通过，仅使用Lean的三个标准公理。

结果的意义在于：它展示了现在可以自动形式化大范围的数学，这可能有助于发现现有数学证明中的错误，并减轻评审新工作的负担。Kevin Buzzard评价称，如果自动形式化FLT现在可行，那么就已经向着自动形式化现代数学文献迈出了一大步。AI辅助形式化也可以帮助验证LLM生成的数学结果。Anthropic认为，形式化将成为与人类可读的论文相伴的常见实践。此外，Claude在编写Lean时似乎能通过部分证明独立检查自己的假设，就像用数值模拟检查推导是否正确。

尽管这是一个token密集的项目（最大的Lean证明），但Anthropic的小实验表明，使用消费者级AI订阅（如Claude Max）在三天内形式化了Vinogradov的三素数定理，说明通过适当框架，协作形式化重大成果是可行的。Anthropic和其他实验室正在扩大对外部研究人员的支持，包括数学形式化项目。