AI完成费马大定理形式化验证，数学审查成本迎来变革

Anthropic于9月4日发布了一项容易被标题误导的研究成果：其Claude模型在Lean证明助手中完成了费马大定理的全流程形式化验证。据官方披露，整个项目耗时11天，生成约1300万行Lean代码，期间共证明30,300个命题，最终证明引用了其中29,500个定理。

这并非意味着AI发现了人类此前未知的数学结论。费马大定理早在1995年就已被Andrew Wiles与Richard Taylor攻克。Claude的实际工作，是将依赖繁复现代数学工具的论证过程，重新转译为Lean能够逐步审核的形式语言。表面上看像是"把答案录入计算机"，实质更接近于把一座仅供专业人士通行的桥梁，拆解为每颗螺栓都必须通过质检的施工图纸。

若认为这条新闻佐证了"AI擅长数学"，那判断方向有所偏差。更准确的解读是：AI正在显著降低数学形式化的技术门槛。人类撰写证明时可以省略直观步骤，直接援引数十年前的结论，依赖读者共享背景认知；而Lean不接受任何"显然"。每条定义、每个类型、每处推导关系都必须显式陈述，系统方可判断结论是否真正由前提推出。

Anthropic官方文章特别强调，本项目的核心价值集中于验证环节，而非新数学发现。Claude的形式化路径沿用了Darmon、Diamond与Taylor对Wiles论证的改进路线。数十个智能体协同定义概念、推导中间引理，并将这些成果拼接到更高层的定理上。项目还借助Prove2Me维护定理依赖关系图，使各智能体明确后续任务方向，并缓解长链路任务中的上下文丢失问题。

规模层面同样传递出重要信号。最终代码量约1300万行，达到Mathlib主库规模的五倍以上；这并不说明机器证明比人类版本"精妙五倍"，而是体现了机器审核对显式细节的高度依赖。官方同时披露，早期失败尝试约占最终非模板代码的7%。这恰好表明：自动化并未消除试错，只是将试错转化为可执行、可回退的工程流程。

对数学家群体而言，这项工作价值或将体现在审稿阶段。形式化证明虽不能取代人类的深度理解，但能将"是否在某步出现推理错误"这一判断，转化为计算机可重复执行的核查操作。对开发者而言，实际资源消耗也远不止token费用：还包括证明助手配置、数学库调用、任务拆分、状态追踪、编译算力以及人工抽查。Anthropic披露本次项目消耗约60亿输出token，这表明AI形式化更适合应用于高价值、可复用的数学基础设施建设。

本项成果最值得关注的，并非"Claude击败了数学家"，而是展现了一种全新的分工模式：人类负责提出问题、规划路线并评估数学意义，AI承担将庞大推导过程拆解并交由形式系统逐项审核的任务。数学结论的可信度，有望借此获得一条更加工业化的生产链路。

参考资料