AI 敢碰 350 年的难题，胆子是 Lean 给的

Hello，我是飞飞。

9 月 4 号 Anthropic 发了篇研究，标题很克制，叫费马大定理的形式化。内容一点不克制：Claude 在 11 天里大体自主干完了这道 350 多年没人啃动的题，写成 1300 万行 Lean 代码，机器检查通过。

我看到的第一反应是例行怀疑。AI 又宣布攻克大难题了，这类话音这几年没少听。

但这回我往下多看了一层，发现真正值钱的点被标题盖住了。

说实话，它跟 AI 聪不聪明关系不大，跟「验证」关系很大。

这道题难在哪

费马大定理的题目，初中生都能看懂：n 大于 2 的时候，a 的 n 次方加 b 的 n 次方，不等于 c 的 n 次方。1637 年费马在书页边上写下它，还顺嘴补了句，我有个绝妙的证明，可惜这地方太小写不下。

然后数学界追了它 350 多年。

追到什么程度？1908 年有人悬赏，光头一年就收到 621 份错误证明。1993 年怀尔斯以为自己证出来了，讲了三天讲座，评审进行到两个月，被人问出一个漏洞，他补了一年才补上。1995 年正式发表的证明，129 页，一群数学家审了好几个月。

这样的故事不止一个。Perelman 的庞加莱猜想证明，社区花了大约四年、外加三份三百页的解读文章，才敢说接受。弱哥德巴赫猜想的证明 2013 年交出去，到今天还在审。数学圈管这个叫验证的税，谁开新证明谁交。

审这么慢，怪不了人。几百页的证明是一根逻辑链条，任何一环松了，后面全塌。想彻底确认，没有捷径，只能一行一行核。

有个叫 Peng 的研究者，读博时的成果差点进 Nature。导师问他，你确定证明是对的么。他答了句实话：99% 确定，但这么长的证明，没法说 100%。

就差这句话，论文没发成。

你看，这道题最贵的部分是验证。证明难，证明「对」更难。

编译器当裁判

那有没有不靠人眼的核法？有，这回的主角 Lean 就是干这个的。

Lean 是一门专门写证明的编程语言。说人话就是：你把数学推理翻译成它认的格式，它逐行检查，对就是对，错一个字都过不了编译。它只认三条数学公理，别的什么都不信。

Anthropic 让 Claude 干的，是把怀尔斯那 129 页的人类证明，翻译成 Lean 认的样子。这活原本是社区工程，Imperial College 的 Buzzard 带数学家干了两年，光前期规划文档就 86 页，预计还要好几年。

Claude 用 11 天跑完了。沿途证明 30300 个定理，最终采用 29500 个。成品 1300 万行，是数学家攒了几十年的证明公共库 Mathlib 的五倍大。

数字念完，最要紧的是这句：检查通过，用的就是那三条公理。另有工具比对确认，它的定理陈述跟 Mathlib 里的标准陈述一字不差。

这 11 天里人干了什么？几乎没干什么。Anthropic 的研究者 Peng 只在旁边偶尔丢两句方向性指令，原话是「Jacobian as a scheme sounds high priority」，雅可比概形这块，听着该优先做；另一句是「Mazur 那块尽早推完」。听上去像老板在群里冒泡，不像在指导证明。

还有个观察值得记一笔。官方说，写 Lean 这件事本身似乎反哺证明能力，Claude 近期的原创结果多半是证明跟形式化并行着写的，它拿形式化当自查手段。这个动作你眼熟么，跟写代码顺手跑一遍测试，是同一个动作。

这就是「机器可验证」的分量。AI 说它证出来了不算数，编译器说了才算。审了一辈子形式化项目的 Buzzard 看完成品，给了句评语：AI 自动形式化的产物，已经健壮到可以被继续搭建了。

头一回跑塌了

这事不是一路顺风。官方写了段挺少见的失败记录。

开跑那次没成。几十个 agent 一开始有些进展，跑着跑着开始丢状态，互相不知道对方干到哪了，协作散了架。失败的尝试，最后只贡献了成品里 7% 的代码。

救回来靠换个平台，叫 Prove2Me，核心就三件事。把所有定理画成一张任务地图，谁证完了、谁还没人领，看得清清楚楚。证明跟陈述分文件放，编译提速。每个定理配一句自然语言说明，方便别的 agent 检索复用。

我跟你讲，我盯着这段失败记录看了很久，因为它太眼熟了。

长任务里 agent 丢状态、协作散架，是我写 agent 运行时那几篇翻来覆去讲的老问题，解法也一模一样：把状态外置成看得见的看板，别指望模型脑子里那点工作记忆。数学域没变什么戏法，就是把土办法用足了。

胆子从哪来

现在把两件事拼起来看。

我给 agent 放权一直放得小心。审它们的活靠三样：diff 逐行过，测试跑没跑通，输出对不对，全是事后验证。没有验证门的活我不放。我那条发稿流水线从选题到排版全是 agent 自动跑，唯独最后推进公众号后台那一按，从没交出去过。

为什么盯着不放，因为我吃过事后验证的亏。有一回部署的 token 悄悄过期，构建全绿，就最后一步推不上去，网站部署红了一整天，我盯着一切正常的界面愣是没发现。还有一回 GitHub token 给得太宽，Claude 顺手改了个我压根没打算动的仓库设置，它是好心，可我事后才发现。没有机器在那儿立刻喊停，验证就全压在我这双懒眼睛上。

以前我当这是胆小。这次的事给我换了个算法：agent 在数学上没有突然变强，变硬的是这个域的验证门。硬到什么程度？一个编译器就能判生死，不占任何人的睡眠时间。

蹦过极的人都懂这个理。敢往下跳，靠的从来不是胆子大，是信那根绳。绳的承重白纸黑字写着，跳的人才敢把步子迈出去。Lean 就是那根能写明承重的绳，所以 agent 在这儿敢跑出 11 天、1300 万行。换成验证门软的地方，改真实的生产库，替人做决定，同样的 agent 就得有人盯着。

所以我那句旧话得补上半句了。我写过野心得配验证，没有验证门的野心不叫放权叫放飞。这回再加一句：验证门有多硬，决定你敢把野心放多大。

想放权，先摸摸你那道门，是编译器级别的，还是扫一眼级别的。

先把冷水备好再留门

封神之前，三盆冷水，官方自己都备好了。

一盆：它没有从零证出来。路线走的是数学家简化好的怀尔斯证明，蓝图和公共库全是社区多年的地基，AI 干的是最后那层翻译和拼装。

二盆：官方自己承认，这 1300 万行比必要的长得多。Mathlib 之所以小，是因为简洁且反复评审过。量大，不等于好。

三盆：全程烧了大约 60 亿 output tokens。官方没换算成本，我也不替它算账。

不过官方顺手做了个小实验，这个得单拎出来讲：三个个人 Max 套餐，agent 全程通过那个任务地图平台协作，三天搞定了另一个定理的完整形式化。也就是说这套打法不挑硬件，门槛正在往普通开发者这边挪。我没复现过，这条你当方向看。

还有个细节我挺喜欢。Claude 干完活，在自己日志里写了句 Historic moment (modulo re-check)。历史性时刻，待复核。

连它自己都先给自己留了道复核的门。

这就是这篇想说的全部：agent 能跑多远，先看绳子有多结实。你手里那道验证门，是编译器级别的，还是扫一眼级别的？评论区聊聊，你敢配多大的野心给它。