被机器翻译的不是天才，而是证明

最容易写出来的标题，是 “Claude 用十一天完成了 Wiles 七年的工作。”

也最容易把事情写错。

2026 年 9 月，Anthropic 公布了一个很重的结果：Claude 基本自主运行约十一天，用 Lean 写出了费马大定理首个完整的、可由计算机逐步检查的证明。Anthropic 把它称为 first complete computer-checked proof。

这当然值得惊讶。

但它和 Andrew Wiles 当年做的事情并不等价。

七年发生了什么#

Wiles 十岁时第一次在图书馆看到费马大定理，后来把它变成了自己成年后的长期执念。PBS NOVA 留下的采访里，他描述那七年秘密工作的方式，很像在一座黑暗的大房子里摸索：先撞上家具，慢慢知道每样东西在哪里，直到某一刻终于找到灯的开关。

那不是一种“把现成步骤抄得更严谨”的劳动。

真正困难的部分，是当时根本不知道下一扇门在哪里。

1993 年，Wiles 宣布证明后，同行审查又发现了一个关键缺口。事情没有因此自动结束。他和 Richard Taylor 继续工作，最后才修补了证明。1995 年正式发表的证明长达 129 页，验证本身也耗费了同行大量时间。

所以 Wiles 七年里最昂贵的东西，并不是写下那些页数。

是发现应该写什么。

Claude 面对的是另一类困难。

数学界已经知道费马大定理为什么成立，也知道一条可以走通的现代证明路线。问题变成：能不能把这套高度抽象、分散在大量数学背景和中间结果里的推理，转换成 Lean 能够逐条验证的形式对象？

形式化不是普通意义上的“翻译文档”。

自然语言数学里，专家会自动补上大量上下文：某个结论为什么可用，某个对象满足什么条件，某一步“显然”究竟依赖哪些前提。到了证明助手里，这些空白不能继续依靠默契。类型要对，依赖要全，中间引理要能够真正拼起来。

过去这件事贵得惊人。

不是因为机器不会检查证明，而是因为人要先把证明整理成机器能够检查的东西。

Claude 这次最值得注意的地方，就在这里。十一天并没有重新发现 Wiles 的数学，但它大幅压缩了把成熟数学转成 machine-checkable proof 的人工成本。

换句话说，它翻译的不是天才。

它翻译的是证明。

“只是形式化”很容易被说成一种降级评价。

但如果把视角从“AI 有没有独立成为数学家”移开，形式化本身其实是一块很重要的基础设施。

一条经过机器检查的证明，不会因为读者疲惫、符号习惯不同，或者某一步被默认成“大家都懂”而放过逻辑缺口。更重要的是，一旦越来越多数学结果进入形式化系统，它们就开始拥有另一种可组合性：定理不只被人引用，也可以被软件可靠调用；新的证明可以站在已有机器验证结果上继续构造。

真正可能发生变化的，是数学知识的验证成本曲线。

过去，形式化大型现代数学往往意味着长期项目、大量专家与非常高的耐心成本。如果这层工作开始被 Agent 持续压缩，未来最先变化的也许不是“数学家还需不需要存在”，而是一些今天根本没人舍得形式化的知识，突然值得被形式化了。

这会影响教材、研究复核、数学数据库，也会影响 AI 自己训练和验证数学推理的方式。

这里仍然应该克制。

Claude 完成一个已知定理的形式化，不等于它独立完成了一次 Wiles 式的数学发现；能够沿着已有路线建立严密形式证明，也不自动说明它已经拥有在未知区域长期发明新概念的能力。

但反过来，把它贬成“自动抄代码”也同样失真。

十一天真正击穿的是另一层旧经验：复杂数学的机器验证，也许不再必然是一项需要很多年人工工程的昂贵奢侈品。

Wiles 的七年仍然是七年。

那七年里，一个人摸黑走进了没有地图的房间。

三十多年后，Claude 做了一件完全不同、但同样会留下后果的事：它开始把那间已经被照亮的房子，重新画成机器也能读懂的地图。