财π新闻 2026年9月5日，Anthropic正式对外公布一项重要研究成果，在清华姚班校友彭天翼的主导下，旗下AI模型Claude仅用时11天，就成功完成了费马大定理的首个端到端机器验证形式化证明。这一成果打破了此前数学界对该类复杂现代数学成果形式化工作的时间预期，相关推进过程与最终产出的各项核心指标，均清晰呈现出AI在数学形式化领域的全新突破能力。

需要明确的是，此次Claude完成的工作并非提出一套全新的费马大定理数学证明，而是将人类数学家已经完成的成熟证明内容，完整翻译转换为计算机可以逐行检查的Lean代码，实现整个证明过程的全链路机器可验证。在整个项目推进过程中，Claude累计生成了约1300万行Lean代码，产出的中间定理数量超过3万个，其中约29500个中间定理被最终的完整证明体系所采用。从代码规模来看，这套由Claude生成的形式化证明代码总量，已经超过了Lean核心数学库Mathlib自身规模的5倍，是迄今为止全球范围内规模最大的一套Lean形式化数学证明。整个工程的推进过程中，累计消耗约60亿个Token，而最终形成的完整证明体系，仅依赖Lean系统的三个标准公理搭建完成，所有推导环节均严格遵循Lean系统的验证规则，不存在任何逻辑断点或未被校验的默认步骤。

为了保障大规模形式化证明工作的有序推进，研究团队在项目开展过程中，专门启用了一套专为数学形式化工作搭建的协作系统Prove2Me。这套系统的核心运行逻辑，是将原本完整的费马大定理证明流程，拆解为由无数个独立定理节点组成的有向无环图，每一个节点都对应一项需要完成的证明任务，节点之间的依赖关系被清晰标注，前序节点的证明完成是后续节点启动的必要前提。依托这套系统，参与项目的多个Claude智能体可以实现高效协同工作，系统会根据不同智能体的运行状态自动分配对应的证明任务，同时所有已经完成验证的定理成果都会被统一存入共享资源池，后续的推导环节可以直接复用这些已经确认正确的结果，避免重复劳动，大幅提升整体推进效率。在整个项目的执行过程中，人类研究人员提供的数学指导内容非常有限，绝大多数的数学定义搭建、中间环节证明推导、任务拆分与不同模块的逻辑拼装工作，都由Claude自主完成，人类仅在极少数关键节点提供了必要的方向校准，没有直接参与具体的代码编写或定理证明工作。

作为本次形式化工作的核心对象，费马大定理拥有极为漫长的研究历史，该定理由法国数学家费马于1637年提出，此后的三百五十多年时间里，无数顶尖数学家投入到相关的证明工作中，整个命题始终困扰着人类数学界，直到1994年才被英国数学家安德鲁·怀尔斯彻底完成证明。在费马大定理提出后的数百年间，一代代数学家从不同方向尝试推进证明进度，欧拉、勒让德、库默尔等知名学者都曾在该领域取得阶段性成果，但始终无法覆盖全部的逻辑环节，直到怀尔斯结合现代数论、代数几何等多个领域的前沿工具，耗费数年时间才最终完成完整证明，其最初公开的证明版本也曾被发现存在关键逻辑漏洞，后续又花费近一年时间才完成漏洞修补，最终形成被数学界广泛认可的完整证明。

在本次Claude的成果公布之前，数学界原本计划以多年社区项目的模式，集合全球各地数学家的力量逐步推进费马大定理的形式化工作，相关项目的第一阶段技术蓝图就长达86页，整个推进周期预计需要耗费数年时间，依靠人工逐步完成每一个环节的代码转换与验证工作。按照传统的形式化工作模式，人工完成一个中等复杂度的数学定理形式化，往往需要耗费数学家数周甚至数月的时间，而费马大定理的证明体系覆盖了代数、调和分析、几何和数论等多个领域的大量前沿内容，涉及的推导环节极为庞杂，人工推进的工作量更是难以估量。此前数学界多个大型形式化项目的推进经验也显示，类似级别的复杂数学成果形式化，往往需要数十名专业数学家协同工作数年才能完成，过程中还可能出现大量反复校验、修正逻辑漏洞的工作，整体推进节奏十分缓慢。

而Claude在本次项目中的表现，完全打破了此前行业内对复杂现代数学成果形式化工作的周期预期，仅用11天时间就完成了原本预计需要数年才能完成的全部工作，最终产出的完整证明体系通过了Lean系统的全链路校验，所有推导环节都可以从三个基础标准公理出发，一步步完成逻辑闭环，不存在任何需要依赖人类经验默认成立的“显然”步骤。这一成果的出现，标志着复杂现代数学成果的自动形式化首次具备了大规模提速的条件，此前被认为需要大量人力投入、漫长周期推进的数学形式化工作，现在可以依托AI的能力大幅压缩耗时，让更多此前被认为难以在短时间内完成形式化验证的大型数学成果，有机会快速完成全链路的机器校验，进一步夯实数学研究的逻辑基础。

整个项目的推进过程中，研究团队也经历了初期的探索阶段，在Prove2Me系统正式投入使用之前，参与工作的多个Claude智能体曾出现丢失项目全局状态、无法有效协同的问题，生成的代码中约有7%的内容属于无效的重复劳动，无法纳入最终的证明体系。而在Prove2Me系统正式启用后，所有的任务节点都被纳入统一的有向无环图管理，每一个智能体的工作进度都可以被实时同步，不同模块之间的依赖关系被清晰梳理，彻底避免了不同智能体重复开展相同工作的问题，也让整个项目的推进节奏变得高度可控，所有中间定理的证明进度都可以被精准追踪，一旦某个节点的验证出现问题，系统可以快速定位对应的依赖环节，及时调整后续的任务分配，保障整个项目在短时间内顺利推进完成。

从最终的成果来看，这套由Claude生成的费马大定理形式化证明，所有环节都严格遵循Lean系统的运行规则，没有引入任何超出三个标准公理之外的额外假设，1300万行代码的每一行都可以被Lean系统独立校验，29500个被采用的中间定理全部通过了机器的逐行检查，不存在任何逻辑漏洞。这一成果没有对怀尔斯已经完成的人类证明做出任何内容上的修改或创新，只是将原本面向人类数学家撰写的、存在大量默认省略步骤的数学证明文本，完整转换为面向计算机的、每一步推导都有明确依据的形式化代码，让整个费马大定理的证明过程实现了完全的机器可复现、可校验，任何使用者都可以通过Lean系统运行全部代码，独立确认整个证明的正确性，不需要依赖顶尖数学家的个人经验来判断证明是否成立。

(编辑：曲昂)