这则消息一出，很容易被读成“AI终于证明了费马大定理”。Anthropic宣布的东西其实更具体：Claude在Lean证明助手中完成了费马大定理的完整形式化证明，耗时11天，过程大体由AI自主推进。人类早就知道费马大定理为真，但让一台机器从可验证的逻辑规则出发，把这条证明重新写成能逐行通过检验的形式化数学，这是第一次。区别很重要：新闻不是讲一个难题终于被攻克，而是在讲一种新的证明生产方式已经成形。
先冷静：它没有证明一个新定理
费马大定理的数学地位没有动摇
费马大定理不是一座才被AI攻下的城堡。1995年，Andrew Wiles发表最终证明，后来又在Richard Taylor的协助下填补了一个关键缺口。自此，数学共同体已经把它当作一个已解决的定理。Claude这次没有推翻旧结论，也没有给出前无古人的灵感式路径。
“已有证明”与“机器可验”之间隔着一整套翻译
Wiles的证明建立在模形式、Galois表示等大量现代数学工具之上。数学论文可以说“这是标准结论”或“由前文直接可得”，读者会接受这些省略。Lean不买账。它要求每一个定义都有明确语法，每一步推理都能从已有定理或公理中走通。曾经被同行评议认可的证明，在Lean看来只是一堆待补全的提示。Claude的任务不是把证明写“对”，而是把证明写“全”。这是1300万行代码之所以存在的原因。
11天、1300万行，工程是怎么展开的
Lean既是语言，也是不近人情的验收者
Claude生成的不是自然语言段落，而是Lean代码。Lean一边读取，一边检查：类型是否一致，引用是否合法，归纳是否覆盖所有分支。任何一步没有通过，整段证明就是无效输出。这里没有“差不多”。模型在Lean面前无法靠修辞加分，只能让代码自身成立。所有“AI说证出来了”的表述，最终都被Lean的验证结果覆盖。
Prove2Me：用验证闭环代替盲目硬猜
Anthropic在这一研究中引入了Prove2Me平台。它的思路不是让Claude一次性吞下整个费马大定理，而是把形式化拆成大量可验证的目标。Claude每给出一个引理或一段证明，验证器立刻给出裁决；通过的留下，失败的退回重来。整个“生成—检查—回溯”的循环里，人类干预被压到很低。真正的裁判不是模型，而是形式化逻辑本身。
30,300个中间定理，构成看不见的脚手架
11天里，Claude证明并记录了30,300个定理，最终主证明链用掉了其中29,500个。这些定理不是从现成数据库里取来的，而是为了打通费马大定理的完整路径，在过程中生成并验证的中间节点。这个规模意味着，AI已经不是在解单道习题，而是在建造一座由形式化命题组成的城市。
规模超过Mathlib五倍，为什么值得再想一层
Mathlib不是小货架，而是形式化数学的公共底座
在Lean生态里，Mathlib是无数人多年维护的数学库，承载着从基础定义到近代定理的庞大积累。Anthropic说Claude这一项目产出的证明规模超过Mathlib五倍。这不是拿小作坊比大工厂，而是拿一次AI自主完成的任务，去对比一个由全球贡献者长期堆叠的公共知识底座。
算力之外，更关键的是维持漫长逻辑链的能力
过去AI定理证明常常停在短引理和题库层面。这次1300万行代码、三万多个可验证命题，要求模型在极长上下文里保持定义一致、依赖清晰、回溯合理。它展示的不再是灵光一现，而是持续构造大型逻辑工程的能力。数学证明第一次呈现出类似软件工程的属性：大型、模块化、可以被版本管理，也可以被机器做回归验证。
下一步的难题不在代码里，在翻译和判断上
机器验证了什么，与证明了什么，不是同一句话
Lean验证的是：从Lean的语言和定义出发，这个形式化命题成立。它不会自动保证形式化表述与自然语言里的费马大定理绝对等价。把数学问题翻译成形式系统，仍然需要人仔细核对。这不是一个操作漏洞，而是理解“机器证明”时必须保留的清醒：验证不等于宣告，逻辑正确不等于语境完美。
数学家真正被改变的，是劳动方式
当一个AI能在11天内把如此庞杂的证明形式化到这种程度，数学界要面对的已经不是“AI会不会下棋”式的表演，而是那些最耗时、最不性感的证明劳动正在被接管。数学家可以更早地把时间放在概念判断、新猜想和反例构造上。费马大定理的代码已经写完，但AI数学的序章才刚刚翻开。
