换算一下，假设一个人类程序员每天工作10小时、全年无休，要敲出这个量级，以每分钟写60行代码的速度，需要将近一整年。而Claude做了这件事，只用了11天。
2026年9月4日，Anthropic宣布了一项让数学界震动的成果：Claude在基本自主运行的状态下，完成了费马大定理首个端到端、经计算机检查的形式化证明。
它没有提出新的证明路线，做的是另一件长期被认为需要数年才能完成的事——把人类数学家写给人看的证明，翻译成计算机能逐行核对的语言。
这个数字背后，藏着一个让很多人不安的问题：如果1300万行代码是AI写的，检查也是机器跑的，那谁来证明这份证明本身没有证错？
11天，29500个定理，一次人类从未见过的工程实验要理解这个问题，得先知道Claude到底做了什么。
费马大定理的原始证明，是安德鲁·怀尔斯在1995年发表的，长达129页。这份证明涉及代数、几何、数论等多个领域，人类数学家验证它需要数月甚至数年。1993年怀尔斯首次公布后，审稿人花了两个月才发现一个关键漏洞，他又花了一年才修补完成。
Claude的事不是重新发明这个证明，而是把怀尔斯的证明，连同它依赖的所有数学基础，转写成Lean语言。Lean是一种证明助手，它不像人类那样可以接受“这一步显然成立”的省略——每一个定义、每一次逻辑跳转、每一个中间结论，都必须被严格写出来。
只要链条中有一环接不上，系统就不会放行。
最终的证明规模说明了一切：1300万行代码，累计尝试证明30300个定理，其中29500个被采纳进最终版本，覆盖了代数、调和分析、几何和数论等多个此前从未被形式化过的数学领域。整个项目消耗约60亿个输出Token，最终代码量达到Lean核心数学库Mathlib的5倍以上。
帝国理工学院数学家Kevin Buzzard，早在2024年就发起了用Lean形式化费马大定理的社区项目，光是第一阶段蓝图就写了86页。数学界普遍预计，完整形式化需要数年。Claude用了11天。
Buzzard本人收到成果邮件时，正在威尔士参加音乐节，信号很差，第一反应是“又一封不靠谱的邮件”。一周后他整理积压的邮件，才知道对方完成了什么。随后，他编译了代码，运行检查工具，确认检查通过。
他的评价是：“这项非凡的自动形式化成果仅用了11天，除了数学公理外没有任何额外假设。”
Lean编译通过，就是“百分之百正确”？Anthropic官方的表态是明确的：“只要Lean最终编译通过，就代表这个证明在逻辑上百分之百成立，没有任何纰漏。”
这个逻辑链条是这样的：Lean的内核是一个基于依赖类型理论的小型可信核，它只接受符合底层逻辑规则的证明项。如果1300万行代码最终通过了Lean的编译检查，那就意味着从最基础的三条标准公理出发，到费马大定理的最终陈述，每一步推理都符合逻辑规则。
没有例外，没有“差不多”。
Anthropic还做了额外验证：用一个比对工具确认，Claude最终证明的定理陈述，与Mathlib库中对费马大定理的定义完全一致。也就是说，它证明的确实是费马大定理，不是一个看起来很像但实际不同的命题。
但这里有一个关键缺口：Buzzard编译了代码，运行检查工具，确认检查通过，但这属于个人验证。
目前公开可查的原始材料包括四样：Anthropic的官方技术博客、GitHub上的完整代码仓库、项目运行的原始思考日志PDF，以及Prove2Me协作平台的技术论文。这四样东西覆盖了从技术宣告到可复现代码资产、从运行过程记录到支撑工具原理的完整链条。
唯一缺失的，就是一份第三方独立机构完成全量Lean校验并公开确认的正式报告。
换句话说，截至2026年9月6日，这份证明通过了Anthropic自己的编译检查，也通过了Buzzard个人的编译检查，但还没有第三家独立机构站出来说：我下载了全部代码，配置了完整Lean环境，从头跑了一遍，确认通过。
这不是怀疑论，这是数学界对“机器验证”这件事应有的严谨。1998年，托马斯·海尔斯证明开普勒猜想后，12位审稿人花了4年审核，最后只能得出“99%可能正确”的结论。海尔斯后来不得不组织二十多人的团队，通过Flyspeck项目耗时多年做形式化验证。
佩雷尔曼的庞加莱猜想证明，数学界花了4年、写了三部数百页的详尽解析才敢确认。哈拉尔德·赫尔夫戈特2013年给出的弱哥德巴赫猜想证明，至今还在同行评审中。
形式化验证被寄予厚望，正是因为它能终结这种“审稿人也不确定”的局面。但形式化验证本身，也需要被验证。
1300万行代码里，有没有人没看到的绊脚石？传播中有一个被放大的说法：“人类基本没插手。”原始官方表述其实是“人类在其中的干预极少，仅仅是Tianyi Peng偶尔给出几句宏观方向提示，比如提示把雅可比作为方案的优先级调高，或者催促尽快推进梅祖尔定理”。
“极少”和“基本没插手”之间，差了一个关键事实：有人在关键节点上做方向选择。这些选择决定了Claude的几十个智能体接下来攻哪个子定理、按什么优先级推进。如果方向选错了，AI可能在一个死胡同里浪费大量算力，甚至生成一套“逻辑自洽但方向偏离”的证明路径。
这是Lean的机制能够兜底的吗？理论上是的。如果方向偏离，最终结论就不会与费马大定理的陈述一致，比对工具会报错。如果逻辑自洽但依赖了不该依赖的假设，Lean也会在编译时发现。
但问题在于，验证'比对工具本身是否正确''编译环境是否正确配置'这些前置环节，目前仍然依赖人类。
一个更微妙的点是：证明的规模。1300万行代码，是Mathlib的5倍。Anthropic自己也承认，这份证明很可能远比实际需要的更长。规模大意味着冗余多，但冗余是不是也意味着有更多角落可能藏着一个未被触发的错误？
这不是说Lean不可靠。Lean的内核经过了数学界多年的检验，规模很小、逻辑清晰，被认为是一个“可信核”。但Claude生成的1300万行代码，是在这个可信核之上构建的。
如果代码中有一个逻辑漏洞，而Lean的编译器恰好因为某个未发现的边界bug没有捕捉到——这个概率极低，但严格来说，不等于零。
数学家们对这件事的态度，在Buzzard的措辞里可以窥见一斑：他用了“非凡的自动形式化成果”，没有用“已被独立验证”或“已被多方确认”。
他确认了代码编译通过，但评价的落脚点是“AI生成的中间产物已经足够稳固，可以层层向上构建”，而不是“这份证明已经没有任何可能出错的空间”。
下一个问题是：当AI生成的证明越来越多，谁来验证验证者？回到最初的问题：谁能证明这份AI完成、机器核验的证明本身没有证错？
目前能给出的最诚实的答案是：有两个人确认了编译通过，但还没有第三方独立完成全量校验。这不是在说这份证明有问题，是在说验证这件事本身，还没有完成它的闭环。
但这件事的意义，恰恰不在于它是否已经“万无一失”，而在于它展示了一条路径：AI负责把人类难以全量核验的复杂证明，转写成机器可以逐行检查的形式；人类负责检查机器检查工具本身是否可靠，以及在关键节点上做方向判断。
这三者——AI的生成能力、形式系统的逻辑守门、人类的判断——结合起来，可能才是未来管理超大规模数学知识的真正方式。
费马大定理的形式化，被数学界预估需要数年。Claude用了11天。下一个问题是：验完这11天的工作，需要多久？