英国数学家安德鲁·怀尔斯于1995年完成的费马大定理证明，近日通过人工智能技术实现了形式化验证。Anthropic公司宣布，其研发的AI模型Claude在自主运行11天后，成功将怀尔斯的证明转换为Lean证明助手可验证的完整形式，生成了超过1300万行代码并验证了3万余个定理。
费马大定理指出，当整数指数n大于2时，不存在满足aⁿ+bⁿ=cⁿ的正整数解。怀尔斯的原始证明长达129页，其正确性曾经历数月人工核查。此次AI项目通过多智能体协作，将证明过程分解为概念定义、中间定理推导和复杂命题验证三个阶段，最终生成的证明规模达到主流数学库Mathlib的5倍以上。
项目负责人Tianyi Peng介绍，团队采用有向无环图（DAG）技术管理定理间的依赖关系，使多个Claude智能体能够并行工作。人类研究人员仅提供高层次指导，如确定数学对象的优先级，具体证明步骤均由AI自动完成。整个过程消耗约60亿个输出Token，使用与Claude Fable 5.1相当的内部研究模型。
Lean证明助手在此项目中发挥关键作用，其严格验证机制要求每个逻辑环节都必须明确表述。这与人类数学证明形成鲜明对比——传统证明常省略被视为"显然"的推导步骤，且依赖大量未形式化的既有成果。项目团队特别指出，此次验证仅使用Lean的3条标准公理，确保了证明的纯粹性。
数学形式化专家Kevin Buzzard审阅后认为，该成果标志着AI辅助数学研究取得重大突破。他指出，将复杂证明转换为计算机可验证形式，过去需要数学家投入数年时间，而AI技术使这一过程大幅加速。Anthropic公司强调，此次验证并非创造新证明，而是展示AI在处理大规模数学形式化任务时的潜力。
完整证明代码已通过GitHub平台公开，供全球数学界核查。该项目验证的简化版本基于Darmon、Diamond和Taylor对怀尔斯证明的优化方案。Anthropic表示，随着AI生成数学成果增多，为传统证明同步提供形式化版本可能成为行业标准，这将显著降低新理论验证的人工成本。
