法国数学家皮埃尔·德·费马在17世纪提出的著名猜想——当整数n大于2时，方程aⁿ+bⁿ=cⁿ不存在正整数解，经过350多年的研究，终于在1995年由安德鲁·怀尔斯完成最终证明。然而，这一数学里程碑的验证过程长期依赖人工审阅，复杂证明的每个环节都需要数学家耗费大量时间追踪依赖关系、验证逻辑链条。如今，人工智能技术为这一领域带来了新的突破。
人工智能研究机构Anthropic宣布，其开发的Claude智能体系统在11天内完成了费马大定理的形式化验证工程，生成约1300万行Lean代码，仅需人类提供少量高层指导。这项工程将怀尔斯的129页证明转化为机器可核验的严格逻辑步骤，通过计算机逐行检查确保无任何疏漏。此前数学界普遍认为，此类大规模形式化工程需要数年时间才能完成。
形式化证明的核心在于将自然语言描述的数学推理转换为证明助手可理解的代码。Lean等工具依据明确公理和规则，对每个逻辑步骤进行严格验证，要求补全人类审稿时可能省略的中间环节。2005年荷兰计算机科学家首次提出将怀尔斯证明形式化的设想，2024年帝国理工学院发起相关社区工程，原计划分阶段实施且周期以年计算。Claude的突破性进展使这一进程大幅提速。
该工程采用多智能体协作模式，数十个Claude实例同时工作，分别负责定义数学概念、证明中间命题、组合高层结论。研究人员开发了Prove2Me协作平台，将待证明定理组织成有向无环图，明确记录任务间的依赖关系。智能体通过该框架判断工作优先级，有效复用已验证结果，避免重复劳动。最终完成的证明仅使用Lean的三条标准公理，经比较工具确认与数学库中的定理陈述完全一致。
工程规模远超现有数学代码库，生成的代码量是Lean核心库Mathlib的五倍以上。虽然存在冗余可能，但成功解决了"能否完整验证"的首要问题。研究团队指出，当前方法在简洁性和可读性方面仍有提升空间，但已证明AI可处理现代数学文献中的大型工程。帝国理工学院数学家凯文·布扎德审阅后认为，该成果可帮助发现现有证明中的错误，减轻人类审稿负担，并严格检查大模型生成的数学结果。
验证环节的价值在本次工程中尤为突出。由于费马大定理已有公认的正确证明，AI的工作重点在于展示自动化形式化的可行性。随着AI参与数学研究，证明产出速度将显著提升，但人类审稿能力难以同步增长。形式化证明提供的机器可核验版本，可使审查者更专注于核心思路和理论价值。不过，Lean等工具仅能验证逻辑正确性，无法自动生成适合人类理解的解释，未来数学成果可能需要同时准备研究者版本和机器验证版本。
小型实验进一步验证了该方法的普适性。研究人员使用三个个人版Claude账号，通过Prove2Me平台在三天内完成了维诺格拉多夫三素数定理的形式化。这表明，只要任务拆解和协作机制成熟，类似工作不限于大型实验室，普通研究团队也可参与。此次工程不仅展示了AI在数学验证领域的潜力，更证明通过合理的外部框架设计，可使多个智能体围绕复杂目标持续高效协作。
完整证明代码及技术细节已公开于GitHub平台，供数学界和计算机科学界审查验证。该项目使用的内部研究模型能力大致相当于Claude Fable 5.1版本，整个任务消耗约60亿个输出Token。研究团队强调，虽然当前成果在代码效率方面仍有优化空间，但已为大规模自动形式化工程的落地实施奠定了重要基础。
