IT之家9月5日消息，Anthropic于当地时间9月4日宣布，其AI模型Claude在基本自主运行11天后，完成了对费马大定理的首个端到端、经过计算机检查的形式化证明。该项目将英国数学家安德鲁·怀尔斯于1995年完成的原始证明转换为Lean证明助手可逐步验证的形式，并非重新发现数学证明。
据介绍，Claude在此过程中生成了约1300万行Lean代码，并证明了约3.03万个定理，其中约2.95万个中间定理被纳入完整证明。整个证明仅使用Lean的3条标准公理，消耗约60亿个输出Token。项目由Anthropic研究员Tianyi Peng发起，通过Prove2Me平台实现多智能体协作，人类仅提供少量高层次指令。
Anthropic强调，此次成果的创新在于利用AI大规模自动完成证明形式化，并由Lean对结果进行验证。完整Lean证明已公开在GitHub上，Kevin Buzzard审阅后认为，AI辅助形式化大型数学成果已取得重要进展。