Anthropic 于当地时间9月4日宣布，其 AI 模型 Claude 在近乎完全自主的运行状态下，历时11天成功完成了费马大定理（FLT）的端到端形式化证明。该证明已通过 Lean 证明助手的计算机检查，成为该数学难题首个被完整机器验证的版本。

这项工作的核心并非重新推导费马大定理的数学证明，而是将英国数学家安德鲁·怀尔斯于1995年提出的经典证明，转化为 Lean 证明助手能够逐步验证的形式化语言。Lean 作为一种专业工具，可逐行检查证明中的逻辑步骤，确保其严谨性。

据 Anthropic 披露，Claude 在此过程中生成了约1300万行 Lean 代码，并验证了约3.03万个定理，其中约2.95万个中间定理被整合进最终证明。整个证明仅基于 Lean 的3条标准公理，由计算机完成全部核验，规避了人工审查可能出现的疏漏。

费马大定理指出，对于大于2的整数指数 n，不存在满足 aⁿ + bⁿ = cⁿ 的正整数解。怀尔斯的原始证明长达129页，其正确性在发表前曾经历数月人工复核。而形式化的难点在于，人类数学证明常省略“显而易见”的推导步骤，但 Lean 要求每个逻辑环节都明确可查。

此次突破展现了 AI 在复杂数学推理中的潜力，尤其为长期悬而未决的数学定理形式化工作提供了新路径。Anthropic 强调，该成果将有助于推动数学研究向更严谨、可验证的方向发展，并可能加速其他领域的形式化验证进程。