9月4日，Anthropic对外宣布，其AI模型Claude在基本自主运行11天后，完成了费马大定理（FLT）的首个端到端、经过计算机检查的形式化证明。这项成果并非重新发现费马大定理的数学证明，而是把已有的人类证明转换为Lean证明助手可以逐步验证的形式。根据Anthropic披露的核心数据，Claude在这一过程中生成了约1300万行Lean代码，证明了约3.03万个定理，其中约2.95万个中间定理最终被纳入费马大定理的完整证明，整个证明由Lean完成检查，仅使用了Lean的3条标准公理。
一、从怀尔斯129页证明到1300万行代码
费马大定理指出，当整数指数n大于2时，不存在满足aⁿ+bⁿ=cⁿ的正整数a、b、c。英国数学家安德鲁·怀尔斯于1995年完成了该定理的证明，原始证明长达129页，其正确性在发表前还经历了数月的人工核查。数学形式化的难点在于，人类数学证明通常会省略大量被认为显而易见的推导步骤，而Lean需要明确验证每一个逻辑环节。此外，数学家长期引用大量尚未被形式化的既有数学成果，因此将完整证明转换为计算机可验证形式通常要投入大量时间，Anthropic此前预计费马大定理的形式化工作可能需要数年。
此次项目最终遵循了Darmon、Diamond和Taylor对怀尔斯证明的简化版本。人类研究人员提供的数学输入主要是少量高层次指令，例如确定某些数学对象或定理的优先级，具体证明过程则主要由Claude完成。研究团队还额外使用比较程序确认，Claude最终证明的数学命题与Mathlib中费马大定理的正式定义完全一致。
与Mathlib中既有定义完全一致，意味着这次工作不是另起炉灶，而是把新证明挂接在Lean社区已经沉淀的术语体系之上。Mathlib相当于Lean生态的公共数学仓库，收录了大量已被形式化验证的基础定理；Claude之所以能把工程压缩到11天，一个重要前提是不必从零证明全部前置结论，而是可以在库中检索、调用已被验证的构件。人类团队在启动前仍需判断哪些结论可直接借用、哪些必须新证，这类对整体数学结构的判断，恰恰是模型暂时难以独立完成的部分。
二、彭天翼与Prove2Me：把大证明拆成一张有向无环图
此次项目由Anthropic研究人员Tianyi Peng（彭天翼）发起。彭天翼2017年从清华姚班本科毕业，2023年获MIT博士学位，早年入选信息学奥赛国家集训队，如今已是哥伦比亚大学助理教授。Claude并非由单个智能体完成全部工作，而是通过多智能体协作完成概念定义、中间定理证明以及更复杂命题的推导。
项目使用了由彭天翼及其哥伦比亚大学合作者开发的Prove2Me平台，用有向无环图（DAG）记录待证明的定理及其依赖关系，并支持多个Claude智能体并行工作。平台会把一个庞大的数学证明拆成一张DAG：最顶层是最终要证明的费马大定理，下面不断拆分为规模越来越小的中间定理。不同Claude Agent分别认领任务——有人定义数学概念，有人证明底层引理，有人利用已完成的结果向上推进。Prove2Me还会记录每个定理的自然语言说明，并允许不同Agent搜索和复用已经完成的结论。
这套机制要解决的核心问题是重复劳动与依赖阻塞：如果没有依赖关系记录，多个智能体很容易各自从零证明同一引理，或在某个前置结论尚未完成时空等；有了DAG和已证结论的检索入口，Agent可以在图上前进、回退、绕行，人类则通过查看图的推进情况判断整体进度，只在关键节点介入。对大型证明项目而言，管理协作本身的开销往往不亚于数学推导，Prove2Me把这一层显式化，正是它能支撑十几个智能体并行推进的关键。
三、3条公理与计算机可检查的意义
整个证明由Lean完成检查，仅使用Lean的3条标准公理，这一点在计算机形式化领域具有指标意义。形式化证明的价值不在于得出新结论，而在于把人类证明中隐含的、被认为显然的跳跃全部显式补齐，让机器逐环验证逻辑。对数学界而言，这意味着一个重要证明在发表后不必再依赖数月人工核查，机器可以在合理时间内给出确定性的正确性背书。Anthropic把原本预计数年的工程压缩到11天，说明多Agent在高度结构化、依赖关系清晰的证明任务上，已经能承担远超单人手工推进的吞吐量。
四、局限与边界
需要明确的是，Claude完成的是形式化（formalization），而非原创数学突破。怀尔斯的证明框架与核心思路仍是人类数学家的成果，Claude的工作是把这套已被接受的数学内容翻译进可机检的逻辑系统。形式化也依赖人类设定优先级、提供高层次指令，并在关键节点做判断。它展示的是AI在“把已有知识变得可验证”这一环节上的工程能力，而非替代数学家提出新定理。
面向创业者与一人公司的行业点评
对一人公司和小型技术团队而言，这次实验的真正启示不在数学本身，而在工程方法论。Prove2Me用一张DAG把超大任务拆成可并行认领的子任务，再让多个Agent复用彼此已完成的中间成果——这套“任务拆解+并行协作+成果复用”的范式，和一人公司用AI团队处理调研、写作、开发的日常逻辑完全一致。当单个Agent的能力上限被任务规模卡住时，把工作流设计成可分解、可追踪、可复用的结构，比继续堆单个模型的上下文更重要。创业者不必等到拥有大团队，就可以借鉴这种思路：把目标拆成依赖图，让多个专项Agent并行推进，人只负责优先级与验收。费马大定理的11天验证，本质上是一次关于“如何用AI组织复杂工作”的压力测试。
本文仅代表作者个人观点（仅供参考） 来源：创客OPC原创整理
