数学界一项延续数百年的工程被AI大幅提速。Anthropic在9月4日发布研究公告，其Claude智能体集群在11天内完成了费马大定理的首个端到端机器可验证证明，全程以Lean语言编写，共产生约1300万行代码并证明29500个中间定理，最终成品规模超过Lean社区核心数学库Mathlib的五倍。这是继AI辅助证明黎曼猜想相关命题后，形式化数学领域又一个标志性节点，其意义不在于发现新的数学，而在于验证本身被彻底自动化。
费马大定理的来历充满传奇色彩。1637年法国数学家费马在丢番图《算术》书页空白处写下断言，任何正整数都无法满足n大于2时的n次方和等式，并称已发现绝妙证明但页边空白写不下。此后的三百五十多年里，无数数学家前赴后继，1908年德国还曾悬赏十万金马克征解，仅第一年就收到621份错误证明。直到1995年，英国数学家安德鲁·怀尔斯才给出长达129页的完整证明，而验证其正确性又耗费了数学界数年时间。
机器形式化的意义正在于把验证从信任问题变成计算问题。所谓形式化证明，是把每一个推理步骤翻译成Lean证明助手能够机械检查的语言，逐行核对直至公理层面，不接受任何凭经验补全的跳跃。帝国理工学院的Kevin Buzzard自2024年起牵头社区项目，原计划用数年时间完成同一目标的从零形式化，此次Anthropic团队在11天内先行撞线，Buzzard亲自编译验证后给出评价，称这项非凡的自动形式化成就仅依赖数学公理即可证明费马大定理，并认为它代表着迈向现代数学文献全面自动形式化的重要一步。
11天完成这一工程的关键在于多智能体协作的规模效应。Anthropic研究员田鹏带领的哥伦比亚大学团队开发了名为Prove2Me的协作平台，平台维护一张定理声明的有向无环图，几十个Claude智能体并行认领图中依赖条件已满足的节点展开证明，每个智能体只需聚焦自己负责的子定理，无需在上下文中装入怀尔斯129页证明的整体结构。声明与证明分离存储降低了重编译开销，每个声明附带自然语言描述便于智能体搜索复用已有引理。
整个运行过程消耗约60亿输出token，由与Claude Fable 5.1能力相当的研究用内部模型驱动。Anthropic还坦诚披露了失败经历，最初直接让智能体对照怀尔斯原始证明推进时，智能体在长程协作中丢失项目状态、协作效率骤降，约7%的非样板代码来自这些失败尝试的痕迹，切换到Prove2Me的共享状态图后问题才得以解决。另一项对照实验显示，三个普通Claude Max订阅用户借助同一平台，仅用三天就形式化证明了维诺格拉多夫三素数定理，说明这类协作方法已具备走向普及的潜力。
围绕此次成果的讨论呈现出难得的理性分层。Buzzard在肯定成就的同时直言，从数学发现的角度看这项工作本质上没有带来新知识，他本人此前对费马大定理的正确性已有99.9%的把握，Anthropic在公告中也主动区分，与近期产生新数学的黎曼猜想研究不同，此次的创新点在于验证，用检查数学证明取代了人工数月乃至数年的评审周期。
这正是形式化验证更深远的价值所在。怀尔斯1993年首次公开证明时，审查者曾发现关键漏洞，他又花费一年才修补完成，人类评审的疏漏在数学史上并不罕见。机器可验证证明从构造上排除了这类风险，只要通过Lean内核检查，每一步推理都严格正确。随着AI以越来越高的频率产出数学成果，自动形式化将减轻评审新结果的负担，帮助人类在扩张的知识版图中维持信任，这也是Buzzard所说的自动形式化技术将带来新工具、剔除现有数学文献中错误的深意所在。反过来看，代码化的证明也让数学知识的存储方式悄然改变，不再依赖个人记忆与纸质文献，而是成为可检索、可复用、可自动链接的公共基础设施。
对Kevin Buzzard这样长期推动形式化的数学家而言，此次成果意味着他原定的多年路线图被大幅压缩。他此前牵头社区项目，计划从零形式化费马大定理的证明，如今AI用11天先行撞线，验证了自动形式化技术的成熟度。在Buzzard看来，AI的价值不在于替代数学家思考，而在于接管证明检查这类高重复劳动，让研究者把时间花在提出新问题上；机器证明与人类论文在表述习惯上差异巨大，社区也需要发展新的审阅与教学方式来消化这类产物，而非简单套用既有的同行评议流程。
对Lean社区而言，1300万行新增代码既是资产也是负担。Mathlib是社区多年积累的公共知识库，此次产出的规模达到其五倍，其中必然包含大量可复用的引理，但也夹杂着只服务于单条证明链的临时构造。如何清洗、组织并让这些代码真正融入社区生态，使后来的数学家能够直接调用而非重新发明，将是比生成证明本身更漫长的工程，也是决定这次技术演示能否沉淀为长期公共财富的关键一步。