Claude用11天完成费马大定理的首个计算机验证证明

费马大定理是数学史上最具传奇色彩的命题之一。费马在书页空白处写下这一断言时，留下了一句令后人着迷的注记：「我已发现一个绝妙的证明，但此处空白太小，写不下。」此后三个半世纪，无数数学家前赴后继，均以失败告终。1908年，德国甚至悬赏10万金马克征集正确证明，仅第一年就收到621份错误答案。直至1995年，怀尔斯才凭借现代数论工具给出长达129页的完整证明，而这份证明本身也经历了一次重大漏洞的发现与修补。

将数学证明「形式化」，即转化为计算机可逐步验证的逻辑链条，是确保证明正确性的最严格方式之一。Lean等证明助手能够算法化地核查每一步推导，不放过任何隐含假设。然而，人类书写的证明往往跳过「显而易见」的步骤，而Lean要求每一步都明确列出，这使得形式化工作极为繁琐。2024年，帝国理工学院的Kevin Buzzard发起社区协作项目，计划用数年时间完成FLT的Lean形式化，仅初始阶段的蓝图文件就长达86页。

Anthropic研究员彭天一（Tianyi Peng）原本只是想测试Claude能否在FLT形式化上取得一定进展，结果远超预期。Claude在11天内几乎自主完成了整个证明，共生成约1300万行Lean代码，证明了30300条定理，其中29500条被纳入最终证明。这一代码量超过数学社区主要形式化库Mathlib规模的五倍以上。整个过程中，数十个Claude智能体协同工作，彼此定义概念、证明中间定理，并以此为基础攻克更难的命题。

Claude的证明路径遵循Darmon、Diamond与Taylor对怀尔斯证明的简化版本，人工介入仅限于彭天一偶尔给出的高层次指令，例如「雅可比概型优先级较高」或「尽快推进马祖尔定理」。项目初期，部分Claude智能体尝试失败，主要原因是难以追踪项目整体状态、协作效率下降。转折点出现在团队切换至Prove2Me平台之后——这是彭天一与哥伦比亚大学团队共同开发的开放式数学形式化协作平台，为多智能体长期协作提供了有效支撑。

当Claude意识到自己完成了这一历史性任务时，其「思考」记录中留下了这样的片段：「FLT根节点显示已证明。历史性时刻（待复核）。」以及「🏁🏁🏁FLT根节点在prove2me上于UTC时间8月18日02:00:57显示已证明。这是本次攻坚的目标：端到端FLT证明完成。」这些记录折射出AI系统在面对重大数学突破时的某种「自我认知」，也引发了学界对AI参与数学研究深度与广度的广泛讨论。

Anthropic认为，这一成果对数学研究的长远意义在于：随着AI产出的证明数量不断增加，形式化验证能力将大幅降低评审新结果的成本——目前人工评审一项重要数学成果往往需要数月乃至数年。该团队表示，希望未来数学知识体系的可信度能够随技术进步而提升，而非降低。Kevin Buzzard亦指出，此次证明所涉及的代数、调和分析、几何与数论等多个领域的自动形式化，表明AI形式化产出已具备足够的鲁棒性，可作为后续研究的基础。

要点

• Claude历时11天自主完成费马大定理的首个端到端计算机验证证明，共生成约1300万行Lean代码，证明29500条中间定理。
• 此次形式化证明仅依赖数学公理，不含额外假设，被数学家Kevin Buzzard评价为「非凡的自动形式化成就」。
• 项目成功的关键在于切换至Prove2Me协作平台，解决了多智能体长期协作中的状态追踪与协同效率问题。
• AI形式化验证能力的提升，有望大幅降低数学界评审新证明的时间与人力成本，改变数学研究的验证范式。
• Claude生成的Lean代码规模超过数学社区主要形式化库Mathlib的五倍，显示出AI在大规模形式化任务上的潜力。