Claude自动完成费马大定理形式化证明

近日，Anthropic宣布其旗下AI模型在基本自主运行11天后，成功完成了对费马大定理的首个端到端、经过计算机检查的Lean形式化证明。这一成果并非由AI重新发现该定理的数学证明，而是将已有的数学证明转换为Lean证明助手能够逐步验证的形式。Lean是一种用于编写和验证形式化数学证明的证明助手，能够通过计算机检查证明中的逻辑步骤。

在这一过程中，Claude生成了约1300万行Lean代码，并证明了约3.03万个定理，其中约2.95万个中间定理最终被纳入费马大定理的完整证明。整个证明由Lean完成检查，仅使用了Lean的3条标准公理。这项工作的目标是将英国数学家安德鲁·怀尔斯于1995年完成的费马大定理证明进行形式化。费马大定理指出，当整数指数n大于2时，不存在满足a^n + b^n = c^n的正整数a、b、c。怀尔斯的原始证明长达129页，其正确性在发表前经历了数月人工核查。

数学形式化的难点在于，人类数学证明通常会省略大量被认为显而易见的推导步骤，而Lean需要明确验证每一个逻辑环节。此外，数学家长期以来会引用大量尚未被形式化的既有数学成果，因此将完整证明转换为计算机可验证形式通常需要投入大量时间。Anthropic此前曾预计费马大定理的形式化工作可能需要数年时间。

此次项目由Anthropic研究人员Tianyi Peng发起。Claude并非由单个智能体完成全部工作，而是通过多智能体协作完成概念定义、中间定理证明以及更复杂命题的推导。项目使用了由Peng及其哥伦比亚大学合作者开发的Prove2Me平台，用有向无环图记录待证明的定理及其依赖关系，并支持多个Claude智能体并行工作。最终证明遵循了Darmon、Diamond和Taylor对怀尔斯证明的简化版本。人类研究人员提供的数学输入主要是少量高层次指令，例如确定某些数学对象或定理的优先级，具体证明过程则主要由Claude完成。

整个项目消耗了约60亿个输出Token，使用的是一个与Claude Fable5.1大致相当的通用内部研究模型。最终生成的证明规模超过Mathlib这一主要数学证明库的5倍。Anthropic特别强调，此次成果的重点并不是AI独立提出了新的费马大定理证明，该定理早在1995年已由怀尔斯证明，此次工作的创新之处在于利用AI大规模自动完成证明形式化，并由Lean对最终结果进行计算机验证。

Anthropic认为，如果类似的自动形式化技术能够扩展到更多现代数学成果，就有望降低数学研究中验证新证明的人工成本。随着AI生成数学成果的数量增加，为面向人类阅读的数学证明同时提供形式化版本，未来可能成为常见做法。此次项目的完整Lean证明已经公开在GitHub上。同时，数学家Kevin Buzzard对该证明进行了审阅，并认为这项自动形式化成果显示，AI辅助形式化大型数学成果已经取得重要进展。