近日，英国数学家安德鲁・怀尔斯于1995年完成的费马大定理证明，经Anthropic公司的AI模型Claude自主运行11天后，成功完成形式化验证。该过程生成了超过1300万行代码，并验证了3万余个定理。项目采用多智能体协作和有向无环图技术来管理定理间的依赖关系，人类仅提供高层次指导，全程消耗约60亿输出Token，使用的是Claude Fable 5.1级别的内部模型。Lean证明助手凭借其严格的验证机制参与其中，仅用3条标准公理就确保了证明的纯粹性。数学形式化专家认为，这是AI辅助数学研究的一次重大突破，过去需要数学家数年才能完成的复杂证明形式化工作，现在被AI大幅加速。完整的证明代码已在GitHub上公开，Anthropic表示，未来为传统证明同步提供形式化版本或将成为行业标准，从而降低新理论验证的人工成本。