Anthropic的Claude用11天干完人类计划10年的活，把费马大定理拆解成了1300万行可验证的计算机代码！
这件事改写的不只是数学证明的速度，整个数学界的规则都在悄悄松动！
费马大定理问世三百多年后，Claude借助Lean证明助手，在11天内完成该定理的全流程形式化验证，产出1300万行代码。这项工程远超人类协作的效率边界，也给数学同行评议体系带来全新的冲击与思考。
人类证明靠同行信任，Lean只认代码逻辑
1993年，英国数学家安德鲁·怀尔斯站在剑桥大学的演讲台上，当众宣布自己证明了费马大定理。在场的学者集体起立鼓掌，数学界都以为这个悬置三百多年的难题就此落定。
没过多久，负责审稿的数学家就在证明里发现了一个关键逻辑缺口。怀尔斯退回书房，又花了足足十四个月修补漏洞，才最终拿出完整可信的证明。这个小插曲暴露了一个常人很少留意的事实：数学证明的“发表”和“成立”之间，隔着一条靠信任填充的鸿沟。
人类数学家读论文的方式，和普通人读小说没有本质区别：遇到“显然可得”的推导，读者就默认步骤成立；遇到“根据某某定理”的引用，读者就默认定理适用。这套体系运转了几百年，靠的是同行间的学术信誉，靠的是造假的代价高到没人愿意触碰。
但是，Lean证明助手的出现，直接抽走了这条信任基石。
你可以把Lean理解成数学世界里的超级严格编译器：数学家把每一步推导都写成Lean能识别的规范代码，它就会逐行核对逻辑；这个结论能不能从前面的步骤里合法推导出来，不能的话直接报错，半分情面都不会讲。
人类说“我证完了”不算数，Lean打出“检查通过”的标记才算数！这就带来了一个夸张的工程难题：怀尔斯的原始论文只有129页，可它用到的前置理论横跨代数数论、模形式、伽罗瓦表示等多个领域，要把这些内容全部翻译成Lean代码，工作量远超任何一个数学家的毕生精力。
帝国理工学院的数学家凯文·巴扎德在2024年牵头启动了这个翻译项目，他当时预估，整个团队做完这件事至少需要10年。
Claude只用了11天。
1300万行代码背后，是两万多级数学台阶
Claude最终产出的代码总量达到1300万行，累计证明了约三万零三百个数学定理，其中两万九千五百个属于“中间定理”。
这个数字不能只看表面，得拆开才能看懂它的分量。人类数学家写证明时，可以自由引用已有的公认结论。你在论文里写“根据费马小定理”，不需要把费马小定理的证明过程再写一遍，同行默认这个结论是对的，也默认你用对了。
但Lean不认这套默认规则。你要引用费马小定理，就得先把费马小定理在Lean里完整证明一遍，通过检查之后才能调用。每一个前置概念，每一个被引用的定理，每一步推导的逻辑规则，都必须有对应的Lean代码做支撑。
这意味着Claude做的工作远不止“翻译怀尔斯的论文”这么简单！它相当于从最基础的皮亚诺公理开始，把通往费马大定理的整条数学知识链条，完完整整在Lean系统里重建了一遍。
那些中间定理，就是这条长链上的一个个台阶。两万九千五百个中间定理，等于搭出了两万九千五百级严格验证过的阶梯，每一级都必须稳稳立住，上面的所有推导才能成立。少了任何一级，整个证明都会直接坍塌。
这也是1300万行代码体量惊人的原因。Lean官方有一个由全球数学家花了十几年手工维护的核心数学库Mathlib，Claude在11天里写出来的代码量，是整个Mathlib规模的五倍还多。
但是，这项看起来碾压人类的工程成果，藏着一个让很多数学家心里发闷的事实。
代码验证全通过，数学家却读不懂逻辑
凯文·巴扎德审阅完Claude的成果后给出了明确结论：以前他有百分之九十九点九的把握认为怀尔斯的证明是正确的，现在他有百分之百的把握。
这是极高的认可，却不是故事的终点。巴扎德同时指出，Claude生成的代码和人类维护的Mathlib完全不同，它堆出了两万九千五百个中间定理，却没法直接被数学家复用。
换句话说，Lean确认这套推导全对，但这套代码的可读性和可维护性是另一回事。人类数学家打开这1300万行代码，看到的是密密麻麻的定义和引理，没有注释，没有章节划分，也没有“为什么要这么推导”的说明。它像一台精密运转的机器，没人能说清这台机器的设计思路。
多伦多大学的数论学家丹尼尔·利特给出了一句评价：如果它能形式化费马大定理，那么它大概就能形式化任何东西。
这句话反过来想更有意思。如果AI能把任何数学证明都形式化、都交给机器验证，那数学家还需要亲手理解那些证明的细节吗？
这已经不是效率问题，这直接触及了数学研究的本质意义。
同行评议要变天，但新麻烦也跟着来了
加州大学圣地亚哥分校的数学家弗雷德里克·曼纳斯点出了当下的行业困境：随着数学论文数量变多、篇幅变长、内容越来越细分，同行评议变得更耗时，效果却越来越差。
传统的同行评议逻辑很简单：你把论文投给期刊，编辑找两三个深耕这个细分领域的专家，花几个月通读全文，判断证明对不对、有没有价值。这套体系在论文少、篇幅短的年代勉强够用，现在却处处卡壳。
现在的数学论文动辄上百页，涉及的细分领域越来越偏，全世界能完全读懂某一篇论文的人，可能连二十个都不到。结果就是审稿周期动辄以年计算，审稿人越来越难找，审稿质量也越来越没保障。
Lean认证提供了一条完全不同的出路。你不需要找懂行的数学家审稿，只需要把证明写成Lean代码，让计算机跑一遍就行。计算机不会累，不会走神，不会因为和作者关系好就放水，它只会一行一行抠逻辑，错了就直接报错。
这听起来像是一劳永逸的解决方案，事情却没那么简单！
Lean只能验证推导过程合不合法，不能判断这个定理本身有没有价值。一个数学家可以写出一篇逻辑完全正确但毫无学术价值的论文，Lean照样会给它打对勾，而同行评议的核心意义，恰恰是判断“这件事值不值得做”。
更麻烦的是前置代码的问题。Claude这次为了验证费马大定理，先形式化了代数数论、模形式、伽罗瓦表示等一大堆前置领域，每一个领域的形式化都是独立的大工程。如果每个数学家都用AI生成自己的Lean代码库，整个领域会变成什么样？
巴扎德直接提出了一个噩梦般的场景：如果AI生成的Lean代码和人类维护的Mathlib互不兼容，数学界会冒出一大堆互不通用的代码库；一个定理在A库被验证了，在B库却没法直接调用；形式化带来的确定性，反而会制造新的碎片化和混乱。
费马的页边玩笑，成了AI的数学体检报告
皮埃尔·德·费马在1637年写下那个著名旁注时，大概率只是随手记了一笔。他说自己发现了一个真正奇妙的证明，可惜书页的边距太窄，写不下。
这个写在页边的小玩笑，折磨了整个数学界三百五十多年，直到怀尔斯在1994年拿出完整证明，才算画上了一个句号。
现在，Claude又把这三百五十多年的数学成果压缩成了1300万行机器代码，让Lean逐行检查完毕。检查是通过了，但这件事的意义，远超过“验证了一个老定理”的范畴。
罗格斯大学的数论学家亚历克斯·孔托罗维奇说，这件事带给他的震撼完全不在“AI证明了定理”，而在于AI展现出了大规模自动形式化大型数学证明的工程能力。
从2024年项目启动到2026年完成，人类预估的工期是10年，AI实际用了11天。这个速度差不是“快一点”和“慢一点”的区别，是“人力极限”和“算力规模”的本质区别。
巴扎德还说了一句更值得琢磨的话：按照当前的发展速度，AI或许不久就能审视人类积累的整个数学知识库，甚至可能发现某些著名结论其实是错的。就在两年前，这还只是个没人当真的幻想。
“发现著名结论是错误的”这句话，戳中了数学界一个心照不宣的默认假设：已经发表的定理，除非出现明确的反例或者错误报告，否则就默认是对的。但这个假设从来没有被系统性验证过，因为没人有精力把人类几千年积累的数学知识，逐行逐句检查一遍。
AI现在有这个精力了。它会找出什么，没人知道。
Anthropic没有说接下来会不会继续做这件事。但Claude已经用实际行动证明，11天就能跑完一条从基础公理到费马大定理的完整验证链条。把这条链条扩展到整个人类数学知识库，在算力层面已经不再是幻想。
这件事的结局还远没有写完。Claude生成的1300万行代码已经在GitHub上公开，但全世界的数学家还在慢慢消化它的分量。巴扎德说，把其中一部分内容整合进Mathlib是有可能的，但对应的工作量同样巨大。
这意味着，AI生成的“不可读但可验证”的数学，和人类维护的“可读可扩展”的数学，这两条路径之间的鸿沟，到今天还没有被填上。
而挖下下一铲土的，不知道会是熬了好几年的人类数学家，还是又一个只用11天的AI。