这几天刷微博和小红书，你大概率刷到过这类标题：“数学界彻底被AI撼动了”“彻底攻克了数学史上的终极噩梦”“数学家们彻底被AGI解放了”。点赞最高的一条冲上900多赞，评论区已经吵起来了：有人担心"解放是好事，解雇可不妙"，有人较真"不可能是60亿token，至少是60b"，还有一位网友默默补了一句：“1995年，安德鲁·怀尔斯证明了。”
最后这条评论，说到了整件事的命门。先把结论放在最前面：Claude没有"证明"费马大定理——这个定理31年前就被人类证完了。Claude干的是另一件事，但这件事反而更值得你看懂。
一、先把真实发生的数字摆齐
9月4日，Anthropic宣布：Claude用11天，完成了费马大定理首个"端到端、经计算机核验"的Lean形式化证明。知乎9月7日Nature跟进报道，到今天（9月8日），知乎上还在冒新的追问，小红书上的笔记标题越来越玄——“它证明了费马，没人看得懂”。知乎小红书
把几组关键数字一次摆齐：
1300万行Lean代码，是Lean社区十年积累的核心库Mathlib（约200万行）的6.5倍，迄今规模最大的Lean证明；
证明了约30300个定理，其中约29500个作为中间引理进入最终证明；
消耗约60亿输出token，用的是Anthropic内部研究模型，能力大致对标Claude Fable 5.1；
最终证明只依赖Lean的3条标准公理，定理陈述与Mathlib自带的费马大定理陈述完全一致，机器核验通过；
帝国理工数学家Kevin Buzzard亲自下载、编译、验证了整个仓库，确认"sorry-free"——没有用占位符作弊，逻辑成立。知乎
数字都很硬。但硬数字之上，叙事已经跑偏了。
二、关键澄清：这是"翻译"，不是"创作"
费马大定理说的是：xⁿ+yⁿ=zⁿ在n≥3时没有正整数解。1637年费马在书页边上写下它，顺嘴留了句"我有一个绝妙的证明，但空白太小写不下"，坑了数学界358年。1995年，怀尔斯用129页的现代数学把它彻底证完——这是数学史的常识，也是那条微博评论纠正的内容。
所以Claude这次做的不是"证明"，而是形式化：把怀尔斯那套"人读得懂、机器验不动"的证明，逐行翻译成Lean证明助手能机械检查的代码。打个比方，这不是写了一本新书，而是把一本外文经典翻译成机器能逐字审计的语言；或者把手写账本改成了每一笔都能自动对账的电子账。
难点在哪？人类数学家写证明会大量省略"显然可得"这类中间步骤，同行靠直觉补齐；Lean不吃这套，每个逻辑环节都必须从公理一步步机械推出。知乎所以这次产出的30300个定理里，绝大多数不是怀尔斯论文里的漂亮命题，而是为了填平人类省略的跳跃、硬堆出来的"脚手架"。
一个容易被忽略的细节：Claude走的不是怀尔斯原版证明，而是Darmon–Diamond–Taylor的简化版本。知乎挑一个结构更规整的重述来翻译，本身就是工程判断——这进一步说明，这是一次工程项目，不是一次数学发现。
三、那它到底牛在哪：把"十年人力验算"压成"11天机器验算"
泼完冷水，该说公道话了。这件事的真正含金量，被"AI证明费马大定理"这个错误标题完全遮住了。
第一，它把一个"不可能任务"的工期打掉了两个数量级。业界此前普遍估计，完整形式化费马大定理需要数年乃至十年。知乎上一个同类工程——开普勒猜想的Flyspeck项目——用了12年、21位研究者。知乎Claude只用了11天。
第二，11天背后的杠杆是工程创新，不是模型突然"更会做数学"了。项目由彭天翼主导（清华姚班本科、MIT博士、现任哥伦比亚大学助理教授），早期多智能体尝试是失败的：Agent之间丢失项目状态、各自为战，拼不成完整证明。破局靠的是Prove2Me平台——把待证定理组织成有向无环图，每个节点是一个中间结论，数十个Claude Agent各领子任务，谁证完一个节点就更新依赖图，其他Agent立刻接力。知乎这套"依赖图+多Agent并行"的打法，才是把数年压成11天的那根杠杆。人类的全部参与，按项目自述，只是彭天翼偶尔说几句方向性的话，比如"Jacobian当作scheme处理，优先级高一点"。知乎
第三，算一笔账。60亿输出token，按当前主流旗舰大模型的对外定价区间粗略折算，大致是几十万元人民币量级（内部模型实际成本无法核实，仅作数量级参考）。用这个钱把"数年至十年的人力验算"压缩成11天，对数学共同体来说其实是笔划算买卖——评论区那位纠结"至少是60b token"的网友，纠结的方向反了：token再多，也比雇几十位顶级数学家干十年便宜太多。微博
四、数学圈的两盆冷水，比任何头条都值钱
第一盆来自Buzzard。 他本人就在牵头社区版的费马大定理形式化项目，等于是被Claude"截胡"的人。他做了最硬核的事——亲自编译验证，然后承认输了这场竞赛。知乎但他的定性同样清晰：这是"自动形式化"已有数学的成就，不产生任何新定理内容，“数学上这成果本质上没有告诉我们任何新东西”。一句话总结整个事件：工程上赢了，数学上空的。 把"形式化"包装成"证明"，就像把"翻译一本外文书"说成"写了一本新书"。
第二盆更锋利，来自菲尔兹奖得主陶哲轩。 他的担忧指向更深处：如果AI把所有试错都内部消化掉，只吐出一个打磨光滑的最终证明，那即使它将来解开了某个开放问题，对数学的增量也有限——因为数学家最珍贵的副产品，往往是那些走不通的路径、失败的尝试和顺带发明的工具。知乎陶哲轩还顺手辟了一个同期谣言：所谓"Claude已经解决纳维-斯托克斯方程"，纯属子虚乌有。这条辟谣本身就是最好的教材：AI能力叙事正在以肉眼可见的速度膨胀。
还有一层归因争议值得你知道。 Anthropic的仓库大量依赖帝国理工已有的FLT项目、Mathlib和第三方工具Prove2Me，"largely autonomous（基本自主）"的说法被认为高估了Claude的角色。而且"11天、60亿token、数十个Agent"这些生产过程描述全部是Anthropic自述——外部能独立确认的只有一件事：存在一个有效的、sorry-free的Lean证明。知乎这不影响成果成立，但提醒你：看到厂商自述的惊艳数字，默认打个"待核实"标签总没错。
五、别把它当孤例：这个月AI+数学在密集爆发
真正该关注的信号是：费马大定理不是终点，甚至不是最高点，而是一条陡峭曲线上的一站。
就在9月8日，南开大学郭少明团队与字节Seed合作，完成了三维粘性挂谷猜想的形式化验证——这是王虹今年7月拿下菲尔兹奖（历史上第三位女性得主）的关键成果。整个工程约180万行Lean代码，其中约90%由Seed Prover完成，代码已在GitHub开源。难点比费马更"新"：挂谷猜想去年才收尾，没有成熟的社区注解和形式化路径可循，依赖的前序论文横跨近二十年。小红书小红书
GPT-6参与了素数间隔研究，把短间隔上界从240压到了186——注意，这条是实打实的新结果。
陶哲轩、Buzzard等参与的Veritas计划已拿下多个里程碑：强素数定理约2.5万行、3周完成；8维和24维球堆积最优性约20万行、3周完成。知乎
把时间轴拉长看：Seed Prover去年7月公开亮相时拿的是IMO银牌分数，一年多之后，它已经在菲尔兹奖级别的真实科研项目里给数学家当形式化助手。
曲线连起来，方向已经很明确：数学验证的瓶颈，正在从"人力太慢"转向"治理太难"。 过去十年最大的障碍是没人愿意花数年一行行写Lean；现在机器一夜能堆出1300万行，新问题随之而来——谁来读懂它、维护它、审计它？知乎上有篇高赞分析说得直白：这是第一次出现"原则上不存在人类读者"的数学真理。检索替代了阅读，证书替代了理解。知乎
六、普通围观者能带走什么：三样东西
第一样，谈资。 下次再看到"AI攻克费马大定理"，你可以一句话终结讨论：AI攻克的不是定理，是验证成本——工程上赢了，数学上没出新东西。这句话的信息密度，够你在任何评论区立足。
第二样，一个三问框架。 以后见到"AI攻克XXX"的爆炸标题，先问三个问题：
出新结果了吗？ 是重新做一遍已有的事（形式化、复现、翻译），还是发现了新东西？两者的意义差着量级。
谁核验的？ 是厂商自证，还是有第三方独立复核？Buzzard亲自下载编译，才算数。
它站在什么肩膀上？ Mathlib、帝国理工的项目、Prove2Me——把这些前人的积累拿掉，"自主"还剩多少？
这三问能过滤掉绝大多数AI膨胀标题。陶哲轩辟谣纳维-斯托克斯那条，就是现成的反面教材。
第三样，三个值得持续盯的信号。 一是"谁来审计机器生成的证明"会变成下一个硬问题——这不止关数学界的事，代码、财报、法律文书，凡是"机器产出+机器核验"的场景都会遇到同款治理难题；二是"多Agent+任务依赖图"这套工程打法，大概率会从数学证明溢出到更广泛的Agent场景，接下来半年，用AI干活的人会陆续感受到它的影响；三是AI产出以"天"计、同行评审以"年"计的剪刀差还在撕裂——弱哥德巴赫猜想2013年被证明后至今没完成期刊正式评审，验证行业本身迟早被AI重做一遍。知乎
1637年，费马在书页边写下那句著名的"空白太小，写不下"。358年后，人类先用129页证明了它，又用1300万行没有人能读完的代码把它讲给了机器听。真理没变，变的是"谁能看懂"。
至于"数学家失业"的恐慌，可以先放一放。知乎上数学家Yuhang Liu把这个真问题挑得很明白：以后顶级数学家可以领导强大的AI快速证明大批定理，那平庸的数学家干什么？知乎——压力从来不在"数学家"这个职业整体上，而在"只会重复劳动"的那部分人身上。这条规律，可不止适用于数学界。
