英国数学家安德鲁·怀尔斯于1995年完成的费马大定理证明，近日在人工智能领域取得突破性进展。Anthropic公司宣布，其研发的AI系统成功将这一长达129页的数学证明转化为计算机可验证的形式化版本，并通过Lean证明助手完成全面核查。这项工作并非重新发现定理证明，而是将人类数学家已完成的证明转换为严格符合计算机逻辑验证标准的格式。
费马大定理指出，当整数指数n大于2时，方程aⁿ + bⁿ = cⁿ不存在正整数解。怀尔斯的原始证明涉及复杂的椭圆曲线与模形式理论，其正确性在发表前经历了数月的人工核查。而此次AI项目仅使用Lean的3条标准公理，就完成了从基础定义到最终结论的全链条验证。整个过程生成约1300万行Lean代码，证明过程中涉及3.03万个定理，其中2.95万个中间定理被纳入最终证明体系。
项目负责人Tianyi Peng博士介绍，这项工作面临两大核心挑战：人类数学证明中大量"显而易见"的推导步骤需要被显式补全，同时需要处理数千条未被形式化的既有数学成果引用。研究团队开发的Prove2Me平台采用有向无环图技术管理定理间的依赖关系，支持多个AI智能体并行工作。Claude系统通过多智能体协作模式，分别承担概念定义、中间定理推导和复杂命题验证等任务，人类研究者仅需提供高层次指导如确定证明优先级。
该项目的计算规模远超常规数学研究，共消耗约60亿个输出Token，使用的内部研究模型与Claude Fable5.1性能相当。最终生成的证明文件规模达到Mathlib数学库的5倍以上，成为目前最大的形式化数学证明之一。为确保结果可靠性，研究团队特别邀请斯坦福大学数学家Kevin Buzzard进行独立审阅，其确认AI生成的证明严格遵循Darmon等学者简化的证明路径。
Anthropic强调，这项成果的核心价值在于开创了AI辅助数学形式化的新范式。传统形式化工作需要数学家手动将证明拆解为计算机可理解的步骤，往往耗时数年。而此次AI系统在11天内自主完成主要工作，证明效率提升超过两个数量级。随着AI生成的数学成果日益增多，同时提供面向人类阅读和计算机验证的双版本证明，可能成为未来数学研究的标准实践。目前，完整的Lean形式化证明已在GitHub平台公开，供全球数学界核查验证。
