文 | Edu 指南
近日，Anthropic 宣布了一项震动数学界的消息：其 AI 模型 Claude 在基本自主运行 11 天后，完成了费马大定理的首个端到端、可由计算机完整检查的形式化证明。
这不是 AI 第一次在数学领域引发轰动。但这一次，震撼程度完全不同。
一个 350 年的 " 页边空白 "
故事要从 1637 年说起。
法国数学家皮埃尔 · 德 · 费马在一本数学书的页边潦草地写下了一句话：对于任意整数 n>2，不存在正整数 a、b、c 使得 a +b =c 。他还补了一句——自己有一个 " 真正绝妙的证明 "，可惜页边太窄写不下。
然后他去世了。
接下来 358 年，一代又一代数学家前赴后继，试图找回费马口中那个 " 绝妙证明 "。欧拉、勒让德、库默尔……无数顶尖头脑折戟沉沙。
直到 1993 年，英国数学家安德鲁 · 怀尔斯公开宣布完成证明。但故事并未就此结束——两个月后，同行评审发现证明中存在关键漏洞。怀尔斯又花了一年时间，与前学生理查德 · 泰勒合作修补，最终于 1995 年发表了 129 页的修正版证明。
怀尔斯的证明是 20 世纪数学的里程碑，为他赢得了 2016 年的阿贝尔奖。但数学家们很快意识到另一个问题：这份写给人类看的证明，计算机看不懂。
从人类直觉到计算机能读懂的逻辑
普通数学论文是写给数学家读的。大量在专业人士看来 " 显而易见 " 的推导会被省略—— " 显然可得 "" 不难验证 " 这类词，背后可能藏着数十个定义、引理，甚至几百年的数学积累。
但计算机没有 " 显然 " 这个概念。它需要一个专门的工具来充当 " 裁判 "，逐行检查逻辑是否成立。
Lean 就是目前最主流的这种工具——它既是一门编程语言，也是一个极度严格的审核者。每一个定义、每一次逻辑跳转、每一个中间结论，都必须被严格写出来喂给它。链条中任何一环有漏洞，Lean 会立刻拒绝通过。一旦通过，就意味着这个证明在逻辑上正确，不再依赖任何人的主观判断。
整个工作的本质就是：把人类直觉上的 " 懂了 "，拆解成机器逻辑上的 " 确认了 "。 这个过程极其枯燥，却又绝对必要。
2005 年前后，计算机科学家已提出将怀尔斯证明 " 翻译 " 给机器的设想。2024 年，伦敦帝国理工学院教授 Kevin Buzzard 正式启动了一个大型开源项目，计划用 Lean 完成费马大定理的机器验证。仅项目第一阶段的技术蓝图就写了 86 页。整个项目预计需要数学家们耗费数年时间。
然后，Claude 来了。
11 天，1300 万行代码
Claude 并非单打独斗。Anthropic 调用了数十个 Claude 智能体并行协作。它们各司其职：有的补数学定义，有的专攻中间引理，有的沿已有成果向更高层定理推进，还有的负责将不同部分拼回整个证明体系。
但一开始，事情并不顺利。Anthropic 发现，当多个智能体直接协作时，它们很快开始 " 失忆 " ——忘记工程进行到哪里、无法复用彼此的结果、协作陷入停滞。
转折点是一个名为Prove2Me的工具，由本次项目的发起者、Anthropic 研究员彭天翼（Tianyi Peng）及其团队开发。Prove2Me 将整个证明拆解为一个有向无环图（DAG），记录每个定理及其依赖关系。每个智能体都能看清全局进度、判断任务依赖、知道自己接下来该做什么，彻底解决了上下文遗忘和协作混乱的问题。
11 天后，结果出炉：
用更直观的方式理解：这些代码若按每页 50 行打印，可铺满 26 万页，相当于 520 本 500 页的学术专著。
整个过程中，人类提供的数学指导极为有限，主要是偶尔给出类似 " 优先完成 Mazur 定理 " 这样的高层方向。
30 万美元买 " 确定性 "
这项成就的成本是多少？
Anthropic 使用的内部研究模型性能大致相当于 Claude Fable 5.1。按该模型每百万输出 Token50 美元的定价计算，60 亿输出 Token 对应约30 万美元——约为 Buzzard 五年期项目经费（100 万英镑）的四分之一。
同时，另一组值得关注的数字是：
五周前，OpenAI 发布了十项专家们至少十年未曾推进的数学难题的突破性成果，每个都附带了可机器验证的 Lean 证书，总成本约2,000 美元。
对比一下：十个真正的数学新发现，成本两千美元；机械确认一个已有三十年历史的结论，成本三十万美元。
Anthropic 对此极为坦诚：Claude 这项工作在数学上 " 没有告诉我们任何新东西 "。怀尔斯已在三十年前完成证明，Claude 只是为它建了一张机器可查验的 " 收据 "。
最贵的从来不是找到答案，而是把答案变成不需要信任任何人、可以被机器逐行验证的形式。
正如《自然》杂志报道所言：一台机器能将人类数学家的工作转化为长达 1300 万行、无懈可击的证明，" 彻底震撼了我 "。
" 如果费马大定理可以，那大概什么都可以 "
数学界的反应复杂而深刻。
Buzzard ——那个本要用数年完成同一项目的帝国理工教授——在审阅后给出了极高的评价：这是一项 " 非凡的自动形式化成就 "，证明过程 " 除数学公理外不依赖任何额外假设 "。他指出：" 如果费马大定理的自动形式化在今天已经可行，那么现代数学文献的全面机器验证就迈出了一大步。"
加拿大多伦多大学数论学家 Daniel Litt 更进一步："如果他们能形式化费马大定理，那他们大概能形式化任何东西。 "
但并非所有人都只有欢呼。
菲尔兹奖得主陶哲轩提出了审慎的观察。他认为，AI 目前在 " 解题 " 和 " 验证正确性 " 前两个层面有优势，但 " 清晰表述 "" 被学术共同体接受 "" 融入学科标准理论 " 等后续环节 " 越来越慢、越来越需要人 "。他警告当前的风险是 "证明消化不良" —— AI 生成速度远超人类理解与教学转化能力。
1300 万行 Lean 代码，没有人能从头通读。" 证明通过机器检查 " 不等于 " 证明适合人类阅读和复用 "。数学知识的可验证性与可理解性正在分离——这是一个新的结构性问题。
11 天，1300 万行代码，30 万美元。
Claude 没有发现新的数学定理，但它做了一件可能同样重要的事：证明了一个 AI 可以将人类最复杂的数学成果，转化为机器可以独立验证的形式。
Buzzard 有句话说得恰到好处：" 两年前，这还是个幻想。"
而今天，这个幻想变成了 1300 万行可以逐行检查的代码，安静地躺在 GitHub 上，等待任何一个有足够时间和好奇心的数学家去翻阅。
费马大定理的形式化，或许只是一个开始。真正的问题不是 "AI 能不能做到 "，而是——当 AI 能以人类无法企及的速度生成可验证的知识时，我们准备好了吗？
