AI世界数学里程碑：Claude仅用11天完成费马大定理端到端形式化证明

核心内容

{'title': 'AI世界数学里程碑：Claude仅用11天完成费马大定理端到端形式化证明', 'source': 'AIbase', 'date': '2026-09-07', 'summary': 'Anthropic近日宣布，其AI模型在自主运行11天后，成功完成了对费马大定理（FLT）首次端到端、计算机可检查的Lean形式化证明。该工作并非由AI重新发现该定理的数学证明，而是将已有的数学证明转换为可由Lean证明助手逐步验证的形式。Lean是一种用于编写与验证形式化数学证明的工具，能够通过计算机检验证明中的逻辑步骤。在此过程中，Claude生成了约1300万行Lean代码，证明了约30300个定理，其中约29500个中间定理最终被纳入费马大定理的完整证明。整个证明由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辅助大型数学成果形式化的重要进展。', 'tags': ['AI', 'Claude', 'Anthropic', '费马大定理', '数学形式化', 'Lean'], 'image': 'https://upload.chinaz.com/2026/0907/6392439125393533479811886.png'}