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