费马大定理，这个困扰数学家三个半世纪的难题，在1995年被英国数学家安德鲁·怀尔斯用129页纸证明。而就在本周，Anthropic宣布其AI模型Claude用11天时间，完成了这个定理的首个端到端、经过计算机检查的形式化证明。
这不是AI重新发现了数学证明，而是把已有的证明翻译成了计算机能逐步验证的语言。整个过程中，Claude生成了约1300万行Lean代码，证明了约3.03万个定理，其中约2.95万个中间定理被纳入了最终证明。整个证明由Lean完成检查，仅使用了Lean的3条标准公理。
为什么这件事值得关注？
先解释一下背景。Lean是一种形式化证明助手，它能通过计算机检查证明中的每一个逻辑步骤。人类数学家写证明时，通常会省略大量"显而易见"的推导步骤——这些步骤对人类读者来说不需要解释，但计算机需要明确验证每一个环节。
这正是数学形式化的核心难点。怀尔斯的原始证明长达129页，发表前经历了数月的人工核查。要把这样的证明转换成计算机可验证的形式，数学家们长期以来需要投入大量时间，因为还要引用大量尚未被形式化的既有数学成果。Anthropic此前预计，这项工作可能需要数年时间。
Claude是怎么做到的？
这次项目由Anthropic研究员Tianyi Peng发起。Claude并非由单个智能体独立完成，而是通过多智能体协作完成概念定义、中间定理证明以及更复杂命题的推导。项目使用了Peng及其哥伦比亚大学合作者开发的Prove2Me平台，用有向无环图（DAG）记录待证明的定理及其依赖关系，支持多个Claude智能体并行工作。
人类研究人员的角色主要是提供高层次指令——比如确定某些数学对象或定理的优先级，具体证明过程则主要由Claude完成。最终证明遵循了Darmon、Diamond和Taylor对怀尔斯证明的简化版本。
整个项目消耗了约60亿个输出Token，使用的是一个与Claude Fable 5.1大致相当的通用内部研究模型。最终生成的证明规模超过Mathlib——这个主要数学证明库——的5倍。
正方观点：AI辅助数学验证的转折点
Anthropic认为，如果类似的自动形式化技术能扩展到更多现代数学成果，就有望降低数学研究中验证新证明的人工成本。随着AI生成数学成果的数量增加，为面向人类阅读的数学证明同时提供形式化版本，未来可能成为常见做法。
伦敦帝国理工学院的Kevin Buzzard对这次证明进行了审阅，他认为这项自动形式化成果显示，AI辅助形式化大型数学成果已经取得重要进展。
反方观点：这不是"AI证明数学"
Anthropic特别强调，此次成果的重点并不是AI独立提出了新的费马大定理证明。该定理早在1995年已经由怀尔斯证明，此次工作的创新之处在于利用AI大规模自动完成证明形式化，并由Lean对最终结果进行计算机验证。
换句话说，Claude做的是"翻译"和"验证"工作，而不是"发现"工作。它没有提出新的数学思想，只是把已有的证明变成了计算机能检查的形式。这更像是给数学证明装上了一道自动质检流水线，而不是让AI成为数学家。
我的判断：形式化是AI数学的必经之路
这次成果的意义在于证明了"规模可行"。1300万行代码、3万个定理、11天——这些数字说明，AI自动形式化大型数学成果已经从理论变成了现实。虽然它没有解决新的数学问题，但它解决了"如何让计算机验证复杂证明"这个工程问题。
对于数学界来说，这意味着未来验证新证明的人工成本可能大幅下降。对于AI行业来说，这展示了多智能体协作在长周期、高复杂度任务上的潜力。完整的Lean证明已经公开在GitHub上，任何人都可以查看和验证。
费马大定理的形式化完成，不是终点，更像是一个起点——它证明了AI可以处理人类数学中最复杂的证明结构，剩下的问题是：下一个被形式化的，会是什么？
热门跟贴