本文选自 Horizon 2026年9月5日技术简报。
关键词：Claude、Lean 4、费马大定理、形式化验证、Prove2Me、多智能体、AI for Science
2026年9月4日，Anthropic公布了一项很容易被“AI又攻克一道数学名题”这种标题掩盖掉技术含量的工作：一个由Claude驱动的多智能体系统，在11天内完成了费马大定理（Fermat’s Last Theorem，FLT）的端到端Lean形式化。官方披露，整个项目生成约1300万行Lean代码，完成30300个可机器验证的定理，最终证明使用了约29500个中间定理，消耗约60亿个输出Token。
这里最值得关注的并不是费马大定理本身。怀尔斯与泰勒在1990年代已经完成数学证明，Anthropic也明确说明，这次工作没有提出一条新的FLT数学证明路线，而是把Darmon、Diamond与Taylor对Wiles—Taylor—Wiles证明的整理版本转换成Lean可以逐步检查的形式化对象。技术突破出现在另一个方向：过去需要由少数熟悉高等数论、代数几何和证明助手的专家长期推进的形式化工程，被拆成了大量可以并行调度、自动验证、反复重试的智能体任务。
这件事对AI科研的意义，可能比“模型能不能解一道更难的题”更大。它展示了一种新的研发结构：模型负责高速生成候选推理与形式化代码，证明助手负责提供严格的机器验收，任务图负责管理数万项依赖关系，人类只在少量关键节点提供方向判断。AI输出第一次具备了接近大型软件工程持续集成的验证闭环。
一、为什么把一个已经证明的定理写进Lean，仍然非常难
数学论文中的证明和计算机可以检查的证明，实际上是两种完全不同的工程对象。
数学家写论文时会省略大量被认为“显然”的步骤。一个代数变换可能只写一句“由标准结论可得”，一个几何对象可能直接引用几十年前的文献，一段论证又可能建立在读者默认掌握的若干定义、引理和约定之上。同行评审的工作方式，是由专家理解作者意图，确认这些省略不会破坏整体逻辑。
Lean等交互式定理证明器没有这种默契。它需要明确知道对象的类型、定义域、前提、依赖定理和每一步逻辑变换，并最终由一个规模相对小、可信边界清晰的内核检查证明项。某一步在人类看来只需几秒钟确认，在Lean中可能需要补齐十几个中间引理；论文引用一个成熟理论，形式化工程则可能需要先把该理论所需的大量基础设施补进库中。
费马大定理尤其麻烦。现代证明并不是围绕方程 a^n+b^n=c^n 直接做初等数论变换，而是经过椭圆曲线、模形式、伽罗瓦表示、变形理论以及一系列深层结构，把一个看似初等的整数方程问题映射到20世纪数论建立起来的大型理论体系中。也就是说，要让Lean检查FLT，项目团队需要把相当大一部分现代数论的“隐含知识”显式化。
Anthropic披露的1300万行Lean代码正说明了这一点。这个数字不等于人类手写1300万行高质量库代码，其中包含大量机器生成、冗余和后续可以压缩的内容，Anthropic自己也承认最终证明很可能远比必要长度更长。不过如此大的代码量仍说明一个现实：大型数学形式化更像超大规模软件工程，而不是一次性的数学问答。
二、决定项目能否跑通的核心，并非单个模型能力，而是Prove2Me式任务图
Anthropic对项目过程的描述里，有一个细节很关键：早期多智能体尝试并不顺利。多个Agent虽然能够分别解决局部问题，但很快出现项目状态丢失、重复劳动、依赖关系混乱、协作效率下降等问题。最终成功的重要转折，是把任务迁移到Prove2Me这一协同形式化平台。
Prove2Me把一个大证明组织成有向无环图（DAG）。图中的节点是需要证明的定理或中间结果，边表示依赖关系。某个上游引理完成并通过Lean检查后，下游任务立即可以引用；尚未闭合的节点继续由其他Agent尝试。自然语言描述、Lean形式化陈述和依赖信息同时被保存，使Agent重新进入任务时无需重新阅读整个工程。
这种设计非常像今天的大型软件研发体系。Git管理版本，构建系统管理依赖，CI负责自动检查，Issue和任务系统管理待办项，而开发者在相对独立的模块上并行工作。Prove2Me把类似结构搬到了数学证明中，只是“编译通过”的标准更加严格：最终必须由Lean内核确认类型和证明项成立。
对长周期智能体尤其重要的是状态外置。大模型上下文再长，也不适合把数万条定理、数百万行代码和长期任务历史全部塞进一次对话。将知识状态、依赖状态、任务进度和验证结果放到外部结构化系统里，Agent只读取当前工作所需的局部上下文，可以显著降低长任务中的记忆退化问题。
这个思路与工业智能体、软件开发Agent、自动化科研平台非常接近。复杂Agent系统的能力上限越来越取决于外部脚手架：任务图怎么拆、状态放在哪里、工具如何调用、失败如何重试、结果如何验收。模型仍然重要，但模型只承担其中一部分。
三、Lean给AI提供了一个极少见的“硬验收器”
今天大多数生成式AI任务都缺少低成本、强确定性的结果验证机制。
写一份咨询报告，评价好坏需要专家阅读；生成一段产品设计，往往要经过用户测试；做科学研究，需要实验、复现实验和同行评审；即使生成程序，也可能因为测试覆盖率有限而留下隐蔽缺陷。模型可以非常快地产生答案，但“这个答案究竟对不对”的验证成本经常成为瓶颈。
形式化数学具有一个特殊优势：候选证明可以由Lean内核自动验收。Agent可以快速尝试大量路径，错误结果直接失败，成功结果则成为后续任务可复用的确定性资产。这使得强化学习、搜索、多Agent并行和自动重试都获得了非常清晰的反馈信号。
从系统工程角度看，可以把流程概括为：
自然语言数学资料 → 定理拆解 → Lean陈述 → Agent生成证明 → Lean编译/内核检查 → 写入证明库 → 解锁下游节点
这里最重要的一步是“验证结果可以反向进入系统状态”。一个通过内核验证的定理不再只是模型的一次回答，而会变成新的可信工具。随着库不断增长，后续任务的搜索空间可能进一步缩小，形成某种正反馈。
这也是为什么形式化验证可能成为AI for Science中非常重要的一块基础设施。未来模型可以同时承担猜想生成、文献阅读、证明探索和形式化工作，而机器检查层负责把“看起来合理”与“逻辑上成立”区分开。
四、60亿输出Token意味着什么：科研Agent开始进入算力密集型工程
Anthropic称整个FLT形式化消耗约60亿输出Token，使用的是一个能力大致相当于Claude Fable 5.1的内部通用研究模型。按照公开API价格简单折算会得到非常高的账面成本，Horizon汇总中给出了约30万美元的估算。不过这类估算只能用于理解量级，内部推理成本、批量任务调度、缓存、失败重试和实际硬件成本不会简单等同于API零售价。
更值得观察的是成本结构的变化。
过去大型形式化项目最大的稀缺资源是专家时间。一个同时理解领域数学与Lean工程的人，需要数月甚至数年维护定义、补齐引理、处理库兼容性。智能体把其中大量“可明确验收、但劳动密集”的工作转换为GPU推理消耗之后，成本第一次可以随着模型价格和推理效率快速下降。
假设同等能力模型单位推理成本未来再下降一个数量级，工具调用和缓存效率持续提高，那么今天只有顶级实验室愿意承担的百万级、十万美元级自动形式化任务，可能很快下降到普通研究团队可以接受的范围。大型旗舰项目与普通科研任务之间本就存在很大的成本跨度，随着工具链成熟，更多局部形式化工作将率先进入普通研究团队可承担的区间。
科研自动化因此会出现一种类似软件开发云化的趋势：复杂课题被拆成可计量的计算任务，研究团队为“机器研究时间”购买算力，而不是全部依赖研究生逐行完成重复性工作。
五、从“会回答数学题”到“能维护知识工程”，评价AI科研能力的尺度正在变化
此前数学能力评测经常围绕奥数题、定理证明benchmark或短程Lean任务展开。这些评测能够测量局部推理能力，却无法反映模型能否连续工作十天、管理几万个依赖节点、修复编译错误、复用其他Agent的成果并最终交付一个大型可验证工程。
FLT项目把评价尺度推向了另一端。它更接近大型研发项目管理，而不是考试。
一个可用的科研Agent至少需要五类能力：首先是理解人类论文与形式定义之间的映射；其次是根据依赖关系拆分任务；第三是使用Lean、搜索、代码库和协作平台等外部工具；第四是从失败日志中定位问题并迭代；第五是把局部成果沉淀成其他Agent可复用的资产。
这五类能力组合在一起，才可能形成长周期自动科研系统。对工业领域同样如此。CAE智能体需要调用网格、求解器和后处理工具；工艺智能体需要访问规则库和历史案例；设备诊断智能体需要连接实时数据、时序算法和知识图谱。只靠一个更大的语言模型，很难承担完整闭环。
六、这项工作的边界也很清楚：机器验证不等于机器理解
Lean证明通过，能够给出很强的逻辑正确性保证，但它不代表整项工作已经自动获得数学意义上的优雅性、可解释性和研究价值。
第一，形式化系统只能验证被写进去的命题。如果定理陈述本身偏离人类真正想验证的问题，证明再严密也没有意义。因此Prove2Me强调对任务核心、定义和里程碑进行人工审核。
第二，1300万行代码反映出目前AI生成形式化证明依然可能非常冗长。对数学家来说，一条好的证明往往还需要揭示结构、给出概念上的解释，并能启发后续研究。机器可检查性解决了“对不对”，没有自动解决“为什么这样做最有价值”。
第三，这次工作主要属于autoformalization，即把已有数学知识转成形式化证明。原创数学发现仍是另一层难题。Anthropic近期也在尝试让模型参与黎曼猜想相关问题等研究，但发现新定理、选择值得研究的方向、判断一个结论的学术价值，都需要不同于形式化转写的能力。
即便如此，形式化这一层仍可能成为未来科研体系的重要基础设施。随着AI产生的证明数量迅速增加，人类同行评审很难同比例扩张。让论文同时附带机器可验证版本，可以把审稿人的精力更多放到创新性、意义和方法选择上，而把大量逻辑核对交给工具。
七、对AI工程更大的启发：先寻找“可验证闭环”，再谈完全自治
从工程视角看，FLT案例最有价值的经验可以概括为一句话：高自治Agent最适合先落到那些结果能够被快速、确定性验证的工作上。
软件工程有编译器和测试；芯片设计有形式验证、仿真与DRC；机械设计有几何约束、有限元求解和制造规则；工业控制可以通过数字孪生和历史数据回放检验策略；数学则有Lean这样的证明内核。只要系统拥有足够强的自动验收器，Agent就可以大胆搜索、并行尝试、失败重来，同时把风险锁在验证边界内。
这比单纯追求“一个模型从头到尾自主完成所有任务”更现实。未来成熟的科研与工业智能体，很可能呈现类似架构：大模型负责规划和生成，领域工具负责计算，知识库负责记忆，任务图负责组织，多Agent负责并行，确定性软件负责验收，人类负责目标与关键决策。
费马大定理的形式化因此可以被看作一个非常醒目的样板。它展示的并非数学家即将退出科研，而是AI开始进入一类过去长期受专家劳动成本限制的知识基础设施建设工作。当推理成本继续下降、形式化库继续扩张、协作平台逐渐成熟后，数学论文“可读版本 + 可执行验证版本”可能会像今天软件项目中的源码与测试一样自然。
到那时，AI对科研最大的改变或许不会体现在某一次漂亮的解题，而会体现在知识生产流程本身：越来越多结论从提出之初，就进入机器可检查、可复用、可追踪依赖的工程体系。
参考资料
- Anthropic, Formalizing Fermat’s Last Theorem, 2026-09-04
https://www.anthropic.com/research/formalizing-fermats-last-theorem - Shuze Chen et al., Prove2Me: An Open Collaborative Platform for Scaling Math Formalization, arXiv:2608.28433
https://arxiv.org/abs/2608.28433 - Prove2Me 官方网站
https://prove2.me/ - Horizon Daily, 2026-09-05 中文摘要
https://thysrael.github.io/Horizon/2026/09/05/summary-zh.html