扯了半年多 Lean我听到“Anthropic 用 Claude 在 11 天内完成费马最后定理的 Lean 形式化证明”这条消息时第一反应不是兴奋而是去找原始说明到底是怎么写的。因为形式化验证这件事最反直觉的地方在于模型能不能“想出”证明远没有它能不能被 Lean 内核接受重要。哪怕模型把推理过程写成了八页花团锦簇的自然语言只要lean命令一跑错就是错对就是对没有任何商量余地。如果你对形式化证明还不熟先把结论放在这里Anthropic 做了一件把“AI 生成数学证明”变成“可机械验证的代码”的事Claude 在其中充当的是工程主力Lean 则充当了那个不讲情面的裁判。这篇文章我想把这件看上去很“神话”的事拆开说说它到底牛在哪、边界在哪以及对你我这种普通开发者和数学爱好者它能留下什么能直接用的经验。1. 为什么费马最后定理是最适合检验 AI 的测试场1.1 证明规模大到必须当软件工程来做费马最后定理FLT说的是当整数 n 大于 2 时方程 a^n b^n c^n 没有正整数解。这句话三百多年没人证出来直到 1994 年怀尔斯Andrew Wiles才拿出完整的证明而且这个证明并不是“一条辅助线”就能讲清楚的东西。怀尔斯证明的核心并不是直接处理指数 n而是用了一个非常绕的思路如果存在反例就可以构造出一条特殊的椭圆曲线Frey 曲线这条曲线应当满足某些性质但不可能成为模形式另一方面半稳定的椭圆曲线又必须满足模性定理两种结论撞在一起就产生矛盾。这条路上横着的东西包括 Galois 表示、模形式、Hecke 代数、岩泽理论……整个证明拆开是几百页论文加上几十个关键引理层与层之间大量互相引用任何一个环节都不能含糊。把这种量级的证明搬进形式化系统简直就像把一个大型分布式系统迁移到新的类型系统里你不仅要确保每个函数能编译还要确保模块之间暴露出来的接口都被正确调用。正因为规模大它才比“证明某个数论小引理”更有资格测试 AI 的长期规划能力、上下文管理能力和错误恢复能力。一个模型如果连 FLT 这种复杂度都能在工具辅助下推进那么它在更小的数学问题上的表现至少不会是因为题目太简单而碰运气。1.2 Lean 不是自动证明器是可验证的“建筑监理”很多人一听到“AI 证明数学”第一反应是模型直接生成一行行的等价式或者计算步骤。但 Lean 的工作方式完全不同它更像一个兼具“编译器”和“数学库”的编程语言数学命题在 Lean 里是有类型的对象证明则是构造这种类型的代码。日常做数学题时我们考究的是推理是否说得通在 Lean 里考究的是表达式能不能通过类型检查。你说你证明了那就拿出一个类型为某个命题的项出来没得商量。这意味着只要 Claude 生成的证明在任何一步有错Lean 都会在控制台里打出红色错误而不是由人抽象地判定它“好像对”。给 AI 用这样的工具做裁判价值在于把“可错性”压到了最低模型无法用话术糊弄你它能依赖的就只有数学库里的定义、引理和逻辑规则。正是因为这一点我反而觉得 FLT 这类验证任务比很多“聊天式 AI 评测”可靠得多。模型做一份卷子人来改分但人的改分标准可能本身就不统一模型去生成一个 Lean 证明改分的不是人而是整个形式化逻辑体系。1.3 智能体循环在这里拥有天然的反馈信号如果把 Claude 当成一个只会“想”的模型那它对数学问题的推理上限会被它的单次上下文长度卡死。但 Anthropic 这类实验几乎不会让模型一次性生成完整证明而是采用智能体循环给模型一个目标让它执行命令观察 lean 返回的结果再让它根据错误信息修改策略再跑。这个循环之所以对 Lean 特别友好是因为 Lean 能提供类似编译器的精确反馈。你写了个 tacticLean 要么说目标被解决要么指出当前目标状态不符合某一引理的前提要么说出不了某个类型依赖。每一句报错都是一条可用的监督信号模型完全不需要靠猜来知道“是不是成功了”。换一个更生活的比喻这很像让一个新人做菜旁边不是站着老师傅用模糊语言指导而是每放一种调料电子秤立刻告诉他“你放多了 3 克”。在这种情况下一个执行意愿强的智能体即使一开始厨艺很烂也能靠高频反馈把经验快速积累起来。Anthropic 的智能体工作流本质上就是把这种“高频反馈”拉满。2. 拆解 11 天里的工作流目标拆解、策略调用与失败回滚2.1 人类先搭证明骨架模型去填内层血肉很多人会以为 11 天是指“Claude 独自完成所有数学推理”的用时但实际操作中工程流程通常都是从一堆已经存在的人类手稿和前人的形式化工作开始的。怀尔斯证明的思路是公开的Lean 社区其实也有不少关于数论、代数几何的 Mathlib 基础设施做垫脚石Claude 要做的是把这些非形式化的数学叙述翻译成一套严格到达每个定义层级的形式语言。从我看到的各种大模型辅助形式化经验看第一周往往不是动笔就写证明而是建立“目标树”。你先把一个巨大的 FLT 定理按证明主路径拆成若干子定理每个子定理再拆成更小可管理的步骤最后落到 Lean 里就是一个又一个以theorem开头的声明。Claude 在这里最消耗时间的工作不是解数学题而是“读文档”它需要理解 Mathlib 中椭圆曲线、模形式、Galois 表示这些概念的具体定义方式否则很容易出现“数学上对的思路但 API 完全拼不上”的情况。这个阶段可以非常残忍。你辛辛苦苦拆出 50 个引理跑一遍发现其中一个引理依赖的另一个引理还没有人形式化过整个任务树就得重新调整。Claude 这项实验中用到的智能体能力恰恰就是在这种反复调整中体现出来的而不是一次性写出一个完美计划。2.2 交互式证明写一条、跑一次、挨一次错、改一下到具体填充证明细节时整个流程就非常像写代码。Claude 会在一个可以执行 Lean 命令的环境里不断提交代码块常用的命令包括apply、exact、rw、simp、linarith、ring_nf等。比如要证明一个非常简单的自然数加法交换律theorem my_add_comm (a b : ℕ) : a b b a : by omegaomega可以自动处理 Presburger 算术一行就结束了。但换成 FLT 里的目标情况会恶心得多。你可能面对的是一个目标⊢ IsModularForm (f q)模型首先要判断该引理可以从哪条模性提升定理退出还要检查f是否满足所有权重、级别、尖点条件。如果当前目标中间有一个条件没有满足Lean 会明确提示缺失的前提Claude 就需要补一个局部引理或者退回到上层去调整证明策略。我实际观察过 AI 在 Lean 里犯错的方式它比人类更爱“试”。人类会觉得某个引理太难思考半天再动笔Claude 会先甩一个simp或者linarith然后等着看报错再换 tactic。这种风格在小型目标上效率惊人但代价是如果某个目标反复失败也会出现完全循环的空转。后来 Anthropic 的机制里应该加上了“失败次数上限”之类的硬约束同一个目标失败太多次就暂停把上下文传给人类或者重新从更大的目标拆解角度思考。2.3 11 天到底是怎么个计时法我一直觉得“11 天”这个数字要谨慎理解它不是单线程模型的纯思考时间也不是一个人打开电脑连续肝 11 天。它更接近一个包含多轮智能体并行执行、自动验证、回归调整的整体流水线时间。因为 Lean 大文件动不动要花数小时甚至更久做全量编译很多时间其实是在等机器跑批处理。你完全可以把它理解成持续集成CI跑了一个大型代码库的工期开发人员不停提交代码CI 不停编译坏了的任务回到队列里由开发人员重新派单。这个“开发人员”可能就是 Claude 的不同会话而不是同一个模型连续思考。数字当然有新闻效果但真正值得看的并不是 11 还是 110而是不管花多久最后摆在面前的是一个 Lean 内核检查通过的结果一个可以回放操作日志的过程。3. Lean 的验证器如何在“幻觉”问题上堵死后门3.1 唯一不能伪造的东西是类型AI 大模型的“幻觉”是个老话题。你让它写数学题它可以自信地编出某个不存在的引理你让它解释代码它也可能把map和fold说反。为什么这次的问题没那么严重因为 Lean 的命题是类型证明是那个类型的项。这个概念对没学过类型论的读者可能有点抽象换个说法在 Lean 里“x y”这种命题本身是一个类型你要构造出一个值来填充这个类型。类型检查器只关心这个值是否合法不关心你写的时候心里觉得自己多有理。当你给了它一段不完整的证明代码它完全有能力告诉你说“抱歉这个类型不是命题所要求的那个类型”或者“你引用了一个未定义符号”。这就导致 Claude 生成的任何后续内容都必须经过严格验证。自然语言幻觉在 Lean 里几乎没有生存空间它要么生成真正可以通过检查的代码要么被编译器按在地上摩擦。我可以毫不夸张地说这是让人工智能介入数学证明最让人安心的部分。3.2 战术层错误可以很温柔但底层内核不会让步Lean 里的证明可以使用高级 tactic 来写比如simp会把目标反复化简ring能做交换环上的多项式等式计算linarith能自动做线性整数/实数算术。对 Claude 来说用 tactic 已经不像在手动构造不可读的 proof term 那么难了。不过tactic 只是帮你生成证明项的“前端工具”最终生成的证明项仍要交给内核检查。内核是一个很小的可信计算基它不接受任何自作聪明的中间假设。也就是说即使 Claude 在by ...块里写了一段看起来像模像样的推理如果最终没法通过后端的类型检查前面写得再像样也白搭。这一点和传统软件开发里的“类型检查 模棱两可”完全不同。类型系统只是在编译层面减少大量 bug但很多业务逻辑仍靠人工测试兜底。Lean 的验证粒度是数学级的这种强约束会让模型养成另外一种习惯宁可把引理拆得更细也不要把大目标一次性交给simp去碰运气。3.3 常见错误类型模型不是在“想数学”更多是在“找 API”下面这张表列出了一些我见过的大模型形式化过程中的典型错误你会发现很多错误和真正的数学能力没有太大关系更像是在强类型语言里做 API 适配翻车。错误类型常见根因Claude 类模型的修复方式unknown identifier引用了 Mathlib 中不存在的常数或引理名用#check或搜索符号确认正确名字目标类型不匹配拿了错误方向的定理或变量没有统一改为apply指定引理显式传递参数前提条件不足缺少某个定义域限制或非退化条件补证额外子目标或改用更强命名的引理tactic 失败simp或rw没有找到重写规则拆分目标或先用have引入中间项超大上下文导致路径遗忘上下文长度挤压导致旧引理不再可见将已经完成的模块封装成顶层 lemma减少模型视野这张表想说的是11 天里很大一部分时间是用在“调试接口”上模型没有时间去质疑费马大定理的数学路线它得不停和 Lean 的工具链、Mathlib 的命名习惯、tactic 的行为细节打交道。这也是为什么形式化验证还远远谈不上“让数学家失业”它更像是一次极其严格、极其冷血的单元测试流水线。4. “完成证明”的真实边界可检查了但还要看依赖和人类复核4.1 你不是从零开始Mathlib 就是那棵大树有朋友看完新闻会问既然 Claude 能证明 FLT那是不是马上什么数学问题都能靠它了答案显然是否定的。这次实验能推进几乎完全建立在 Lean 社区过去几年建立的 Mathlib 上。Mathlib 里已经有大量关于自然数、群论、拓扑、测度、模形式等内容的定义和定理基础。Claude 在做的是站在巨人的肩膀上继续向上爬而不是从地基开始搬砖。这就好比一个人说“我用 AI 三天写出了一个大型电商网站”但这套网站的部署环境里已经预装了数据库、缓存、消息队列和一堆组件库。开发者的确写了关键代码可你不能因此说数据库也是他写的。同样的道理FLT 形式化过程中如果缺少 Mathlib 对某些底层抽象层的支持11 天大概率是不够挥霍的。另外依赖关系本身也有长尾风险。即使最终证明文件跑通了它也依赖一条很长的“引理信任链”。链条最底层由 Lean 内核保证中间层要么已经被其他数学家验证过要么就是这次新写的并被内核接受。任何一个环节的证明文件如果包含sorry严格来说都不能叫完成。所以在看到实验结果时一定要确认整个项目里没有未填充的sorry空洞只跑通主文件某些步骤不能代表整个证明收官。4.2 机器可检查不等于人类“看懂”了每一步我们可以把 Lean 证明理解成一份可执行的源码“能运行”和“运行结果符合预期”不代表代码审查者已经逐行读过并认可其风格。形式化证明同理内核检查保证了逻辑合法但并没有替数学家完成“解释为什么这条路是合理的”这项工作。人类最终解读证明结构时依然要看整体思路。更微妙的是AI 生成的形式化证明往往充满重复劳动。比如它为了绕过一个难缠的边界条件可能连续用了好几个局部引理而这些引理组合出来的效果用人的眼光看完全可以直接用某条更强定理一步带过。换个说法AI 给出的证明可能“能过但很丑”对理解数学并没有太大帮助。这也是为什么很多数学家对“AI 证明”又爱又恨爱的是它补上了许多繁琐的机械步骤恨的是它未必能沉淀出人类可感知的洞见。4.3 所谓“完成”更应该说“这是验证器认证过的版本”如果我们严格定义“完成”那就是存在一组 Lean 文件包含 FLT 语句作为顶层定理整个工程在 Lean 内核检查下无错误通过且没有未完成的sorry。在这个定义下“Anthropic 用 Claude 在 11 天内完成”其实讲的是一个工程里程碑而不是一位数学家获得灵感的瞬间。这种差异非常重要。传统证明的里程碑发生在人的大脑里形式化证明的里程碑则发生在代码仓库里。仓库通过 CI意味着整条证明链条在机械意义上成立但它依然需要维护者不断去理解、回滚、改进。将来如果有人重构了 Mathlib 的某个基础定义这份证明文件很可能会碎掉又需要模型和人类一起重新修。这种“脆弱性”不是 AIGC 的锅而是形式化工程本身的日常。5. 不搞数学的人能从这次实验拿走什么5.1 把形式化验证当成“编译级单元测试”来理解数学证明和软件工程之间的相似性在这次实验里被放得很大。一个定理对应一个需求一个证明文件对应一段代码Lean 内核对应编译器和测试框架。Claude 做了大量“根据报错修复代码”的工作这种工作模式放到公司里的普通业务开发中同样成立。如果你所在的项目有严格的 schema、协议或类型定义你完全可以尝试用 Claude 这类模型去生成实现然后用一套强类型强校验的工具去约束它。模型输出的代码刚跑通并不重要重要的是你能用自动化手段让它对所有边界情况负责。Lean 厉害在它比绝大多数类型系统更严格但它验证严格性的哲学值得借鉴。5.2 给想复现类似流程的人几条实际建议如果你看了这篇也想用 Claude 或类似模型去碰一碰 Lean下面这些建议来自真实踩坑不要一上来就立 FLT 这种巨型目标。先用自然数和初等数论练手比如证整除性质、同余关系把 Lean 和 Mathlib 的基本 API 摸熟。使用项目模板初始化一个 Lake 工程并把 Mathlib 作为依赖。不要在某个临时文件里全靠手里的模型瞎猜#check是你验证符号是否存在的第一道防线。把模型当成“tactic 生成器”而不是“全知数学家”。让它一次只写一个引理或一个证明块然后立刻执行lean编译不要让它一次性吐出整个巨大theorem。遇到错误信息先看变量的类型和作用域。大量失败不是数学不会而是同一个名字在不同引理里被赋予了不同含义。把大证明拆成容易命名的小引理好的命名能让模型后续调用时更轻松。如果你把所有 helper 都叫lemma1、lemma2上下文一长模型就彻底分不清谁是谁了。最后保持“证明文件能跑通”和“这个证明结构是否优雅”两条线同时推进。不要为了通过验证就无脑把问题拆成一地碎片那样以后维护成本会高到让人崩溃。5.3 这件事对软件验证可能带来的后续影响有了这种“AI 生成 形式化验证”的样板我认为接下来会看到更多基础设施性质的落地场景智能合约的逻辑验证、协议的状态机规范、算法伪代码的可执行规范甚至金融系统里的核心计算逻辑。以前这些领域缺少的不是写规范的人而是缺少一个能把这些规范快速变成验证结果的高效生产者。Claude 在 Lean 里生成的证明代码虽然在数学术语上不一定优雅但它既然能被机械检查就说明至少在逻辑层人类要少操很多心。当然现实距离“完全无人值守的自动形式化证明”还非常远。模型依然需要人类定义目标需要人类审查策略也需要大量底层的数学库支撑。但至少 Anthropic 这次用 11 天告诉我们只要裁判足够冷酷AI 的产出就有机会变得值得信赖。我自己的最终体会是别把“AI 证明数学”看成一场取代人类的竞赛它更像我们终于遇到了一种比“让模型自己说什么是对的”更高级的用法——让模型在“必须达到某个客观标准”的环境里持续尝试、撞墙、重来。Lean 就是那堵诚实又坚硬的墙。你问我想不想尝试一次用 AI 形式化“多项式时间的欧拉回路判定”这类小型定理我的回答是随时都想而且建议你也试一次。踩过两轮错误再回头看这篇 Anthropic 的成果你对“11 天”的理解会比看热榜新闻深得多。
AI证明费马最后定理：Claude与Lean形式化验证的11天
扯了半年多 Lean我听到“Anthropic 用 Claude 在 11 天内完成费马最后定理的 Lean 形式化证明”这条消息时第一反应不是兴奋而是去找原始说明到底是怎么写的。因为形式化验证这件事最反直觉的地方在于模型能不能“想出”证明远没有它能不能被 Lean 内核接受重要。哪怕模型把推理过程写成了八页花团锦簇的自然语言只要lean命令一跑错就是错对就是对没有任何商量余地。如果你对形式化证明还不熟先把结论放在这里Anthropic 做了一件把“AI 生成数学证明”变成“可机械验证的代码”的事Claude 在其中充当的是工程主力Lean 则充当了那个不讲情面的裁判。这篇文章我想把这件看上去很“神话”的事拆开说说它到底牛在哪、边界在哪以及对你我这种普通开发者和数学爱好者它能留下什么能直接用的经验。1. 为什么费马最后定理是最适合检验 AI 的测试场1.1 证明规模大到必须当软件工程来做费马最后定理FLT说的是当整数 n 大于 2 时方程 a^n b^n c^n 没有正整数解。这句话三百多年没人证出来直到 1994 年怀尔斯Andrew Wiles才拿出完整的证明而且这个证明并不是“一条辅助线”就能讲清楚的东西。怀尔斯证明的核心并不是直接处理指数 n而是用了一个非常绕的思路如果存在反例就可以构造出一条特殊的椭圆曲线Frey 曲线这条曲线应当满足某些性质但不可能成为模形式另一方面半稳定的椭圆曲线又必须满足模性定理两种结论撞在一起就产生矛盾。这条路上横着的东西包括 Galois 表示、模形式、Hecke 代数、岩泽理论……整个证明拆开是几百页论文加上几十个关键引理层与层之间大量互相引用任何一个环节都不能含糊。把这种量级的证明搬进形式化系统简直就像把一个大型分布式系统迁移到新的类型系统里你不仅要确保每个函数能编译还要确保模块之间暴露出来的接口都被正确调用。正因为规模大它才比“证明某个数论小引理”更有资格测试 AI 的长期规划能力、上下文管理能力和错误恢复能力。一个模型如果连 FLT 这种复杂度都能在工具辅助下推进那么它在更小的数学问题上的表现至少不会是因为题目太简单而碰运气。1.2 Lean 不是自动证明器是可验证的“建筑监理”很多人一听到“AI 证明数学”第一反应是模型直接生成一行行的等价式或者计算步骤。但 Lean 的工作方式完全不同它更像一个兼具“编译器”和“数学库”的编程语言数学命题在 Lean 里是有类型的对象证明则是构造这种类型的代码。日常做数学题时我们考究的是推理是否说得通在 Lean 里考究的是表达式能不能通过类型检查。你说你证明了那就拿出一个类型为某个命题的项出来没得商量。这意味着只要 Claude 生成的证明在任何一步有错Lean 都会在控制台里打出红色错误而不是由人抽象地判定它“好像对”。给 AI 用这样的工具做裁判价值在于把“可错性”压到了最低模型无法用话术糊弄你它能依赖的就只有数学库里的定义、引理和逻辑规则。正是因为这一点我反而觉得 FLT 这类验证任务比很多“聊天式 AI 评测”可靠得多。模型做一份卷子人来改分但人的改分标准可能本身就不统一模型去生成一个 Lean 证明改分的不是人而是整个形式化逻辑体系。1.3 智能体循环在这里拥有天然的反馈信号如果把 Claude 当成一个只会“想”的模型那它对数学问题的推理上限会被它的单次上下文长度卡死。但 Anthropic 这类实验几乎不会让模型一次性生成完整证明而是采用智能体循环给模型一个目标让它执行命令观察 lean 返回的结果再让它根据错误信息修改策略再跑。这个循环之所以对 Lean 特别友好是因为 Lean 能提供类似编译器的精确反馈。你写了个 tacticLean 要么说目标被解决要么指出当前目标状态不符合某一引理的前提要么说出不了某个类型依赖。每一句报错都是一条可用的监督信号模型完全不需要靠猜来知道“是不是成功了”。换一个更生活的比喻这很像让一个新人做菜旁边不是站着老师傅用模糊语言指导而是每放一种调料电子秤立刻告诉他“你放多了 3 克”。在这种情况下一个执行意愿强的智能体即使一开始厨艺很烂也能靠高频反馈把经验快速积累起来。Anthropic 的智能体工作流本质上就是把这种“高频反馈”拉满。2. 拆解 11 天里的工作流目标拆解、策略调用与失败回滚2.1 人类先搭证明骨架模型去填内层血肉很多人会以为 11 天是指“Claude 独自完成所有数学推理”的用时但实际操作中工程流程通常都是从一堆已经存在的人类手稿和前人的形式化工作开始的。怀尔斯证明的思路是公开的Lean 社区其实也有不少关于数论、代数几何的 Mathlib 基础设施做垫脚石Claude 要做的是把这些非形式化的数学叙述翻译成一套严格到达每个定义层级的形式语言。从我看到的各种大模型辅助形式化经验看第一周往往不是动笔就写证明而是建立“目标树”。你先把一个巨大的 FLT 定理按证明主路径拆成若干子定理每个子定理再拆成更小可管理的步骤最后落到 Lean 里就是一个又一个以theorem开头的声明。Claude 在这里最消耗时间的工作不是解数学题而是“读文档”它需要理解 Mathlib 中椭圆曲线、模形式、Galois 表示这些概念的具体定义方式否则很容易出现“数学上对的思路但 API 完全拼不上”的情况。这个阶段可以非常残忍。你辛辛苦苦拆出 50 个引理跑一遍发现其中一个引理依赖的另一个引理还没有人形式化过整个任务树就得重新调整。Claude 这项实验中用到的智能体能力恰恰就是在这种反复调整中体现出来的而不是一次性写出一个完美计划。2.2 交互式证明写一条、跑一次、挨一次错、改一下到具体填充证明细节时整个流程就非常像写代码。Claude 会在一个可以执行 Lean 命令的环境里不断提交代码块常用的命令包括apply、exact、rw、simp、linarith、ring_nf等。比如要证明一个非常简单的自然数加法交换律theorem my_add_comm (a b : ℕ) : a b b a : by omegaomega可以自动处理 Presburger 算术一行就结束了。但换成 FLT 里的目标情况会恶心得多。你可能面对的是一个目标⊢ IsModularForm (f q)模型首先要判断该引理可以从哪条模性提升定理退出还要检查f是否满足所有权重、级别、尖点条件。如果当前目标中间有一个条件没有满足Lean 会明确提示缺失的前提Claude 就需要补一个局部引理或者退回到上层去调整证明策略。我实际观察过 AI 在 Lean 里犯错的方式它比人类更爱“试”。人类会觉得某个引理太难思考半天再动笔Claude 会先甩一个simp或者linarith然后等着看报错再换 tactic。这种风格在小型目标上效率惊人但代价是如果某个目标反复失败也会出现完全循环的空转。后来 Anthropic 的机制里应该加上了“失败次数上限”之类的硬约束同一个目标失败太多次就暂停把上下文传给人类或者重新从更大的目标拆解角度思考。2.3 11 天到底是怎么个计时法我一直觉得“11 天”这个数字要谨慎理解它不是单线程模型的纯思考时间也不是一个人打开电脑连续肝 11 天。它更接近一个包含多轮智能体并行执行、自动验证、回归调整的整体流水线时间。因为 Lean 大文件动不动要花数小时甚至更久做全量编译很多时间其实是在等机器跑批处理。你完全可以把它理解成持续集成CI跑了一个大型代码库的工期开发人员不停提交代码CI 不停编译坏了的任务回到队列里由开发人员重新派单。这个“开发人员”可能就是 Claude 的不同会话而不是同一个模型连续思考。数字当然有新闻效果但真正值得看的并不是 11 还是 110而是不管花多久最后摆在面前的是一个 Lean 内核检查通过的结果一个可以回放操作日志的过程。3. Lean 的验证器如何在“幻觉”问题上堵死后门3.1 唯一不能伪造的东西是类型AI 大模型的“幻觉”是个老话题。你让它写数学题它可以自信地编出某个不存在的引理你让它解释代码它也可能把map和fold说反。为什么这次的问题没那么严重因为 Lean 的命题是类型证明是那个类型的项。这个概念对没学过类型论的读者可能有点抽象换个说法在 Lean 里“x y”这种命题本身是一个类型你要构造出一个值来填充这个类型。类型检查器只关心这个值是否合法不关心你写的时候心里觉得自己多有理。当你给了它一段不完整的证明代码它完全有能力告诉你说“抱歉这个类型不是命题所要求的那个类型”或者“你引用了一个未定义符号”。这就导致 Claude 生成的任何后续内容都必须经过严格验证。自然语言幻觉在 Lean 里几乎没有生存空间它要么生成真正可以通过检查的代码要么被编译器按在地上摩擦。我可以毫不夸张地说这是让人工智能介入数学证明最让人安心的部分。3.2 战术层错误可以很温柔但底层内核不会让步Lean 里的证明可以使用高级 tactic 来写比如simp会把目标反复化简ring能做交换环上的多项式等式计算linarith能自动做线性整数/实数算术。对 Claude 来说用 tactic 已经不像在手动构造不可读的 proof term 那么难了。不过tactic 只是帮你生成证明项的“前端工具”最终生成的证明项仍要交给内核检查。内核是一个很小的可信计算基它不接受任何自作聪明的中间假设。也就是说即使 Claude 在by ...块里写了一段看起来像模像样的推理如果最终没法通过后端的类型检查前面写得再像样也白搭。这一点和传统软件开发里的“类型检查 模棱两可”完全不同。类型系统只是在编译层面减少大量 bug但很多业务逻辑仍靠人工测试兜底。Lean 的验证粒度是数学级的这种强约束会让模型养成另外一种习惯宁可把引理拆得更细也不要把大目标一次性交给simp去碰运气。3.3 常见错误类型模型不是在“想数学”更多是在“找 API”下面这张表列出了一些我见过的大模型形式化过程中的典型错误你会发现很多错误和真正的数学能力没有太大关系更像是在强类型语言里做 API 适配翻车。错误类型常见根因Claude 类模型的修复方式unknown identifier引用了 Mathlib 中不存在的常数或引理名用#check或搜索符号确认正确名字目标类型不匹配拿了错误方向的定理或变量没有统一改为apply指定引理显式传递参数前提条件不足缺少某个定义域限制或非退化条件补证额外子目标或改用更强命名的引理tactic 失败simp或rw没有找到重写规则拆分目标或先用have引入中间项超大上下文导致路径遗忘上下文长度挤压导致旧引理不再可见将已经完成的模块封装成顶层 lemma减少模型视野这张表想说的是11 天里很大一部分时间是用在“调试接口”上模型没有时间去质疑费马大定理的数学路线它得不停和 Lean 的工具链、Mathlib 的命名习惯、tactic 的行为细节打交道。这也是为什么形式化验证还远远谈不上“让数学家失业”它更像是一次极其严格、极其冷血的单元测试流水线。4. “完成证明”的真实边界可检查了但还要看依赖和人类复核4.1 你不是从零开始Mathlib 就是那棵大树有朋友看完新闻会问既然 Claude 能证明 FLT那是不是马上什么数学问题都能靠它了答案显然是否定的。这次实验能推进几乎完全建立在 Lean 社区过去几年建立的 Mathlib 上。Mathlib 里已经有大量关于自然数、群论、拓扑、测度、模形式等内容的定义和定理基础。Claude 在做的是站在巨人的肩膀上继续向上爬而不是从地基开始搬砖。这就好比一个人说“我用 AI 三天写出了一个大型电商网站”但这套网站的部署环境里已经预装了数据库、缓存、消息队列和一堆组件库。开发者的确写了关键代码可你不能因此说数据库也是他写的。同样的道理FLT 形式化过程中如果缺少 Mathlib 对某些底层抽象层的支持11 天大概率是不够挥霍的。另外依赖关系本身也有长尾风险。即使最终证明文件跑通了它也依赖一条很长的“引理信任链”。链条最底层由 Lean 内核保证中间层要么已经被其他数学家验证过要么就是这次新写的并被内核接受。任何一个环节的证明文件如果包含sorry严格来说都不能叫完成。所以在看到实验结果时一定要确认整个项目里没有未填充的sorry空洞只跑通主文件某些步骤不能代表整个证明收官。4.2 机器可检查不等于人类“看懂”了每一步我们可以把 Lean 证明理解成一份可执行的源码“能运行”和“运行结果符合预期”不代表代码审查者已经逐行读过并认可其风格。形式化证明同理内核检查保证了逻辑合法但并没有替数学家完成“解释为什么这条路是合理的”这项工作。人类最终解读证明结构时依然要看整体思路。更微妙的是AI 生成的形式化证明往往充满重复劳动。比如它为了绕过一个难缠的边界条件可能连续用了好几个局部引理而这些引理组合出来的效果用人的眼光看完全可以直接用某条更强定理一步带过。换个说法AI 给出的证明可能“能过但很丑”对理解数学并没有太大帮助。这也是为什么很多数学家对“AI 证明”又爱又恨爱的是它补上了许多繁琐的机械步骤恨的是它未必能沉淀出人类可感知的洞见。4.3 所谓“完成”更应该说“这是验证器认证过的版本”如果我们严格定义“完成”那就是存在一组 Lean 文件包含 FLT 语句作为顶层定理整个工程在 Lean 内核检查下无错误通过且没有未完成的sorry。在这个定义下“Anthropic 用 Claude 在 11 天内完成”其实讲的是一个工程里程碑而不是一位数学家获得灵感的瞬间。这种差异非常重要。传统证明的里程碑发生在人的大脑里形式化证明的里程碑则发生在代码仓库里。仓库通过 CI意味着整条证明链条在机械意义上成立但它依然需要维护者不断去理解、回滚、改进。将来如果有人重构了 Mathlib 的某个基础定义这份证明文件很可能会碎掉又需要模型和人类一起重新修。这种“脆弱性”不是 AIGC 的锅而是形式化工程本身的日常。5. 不搞数学的人能从这次实验拿走什么5.1 把形式化验证当成“编译级单元测试”来理解数学证明和软件工程之间的相似性在这次实验里被放得很大。一个定理对应一个需求一个证明文件对应一段代码Lean 内核对应编译器和测试框架。Claude 做了大量“根据报错修复代码”的工作这种工作模式放到公司里的普通业务开发中同样成立。如果你所在的项目有严格的 schema、协议或类型定义你完全可以尝试用 Claude 这类模型去生成实现然后用一套强类型强校验的工具去约束它。模型输出的代码刚跑通并不重要重要的是你能用自动化手段让它对所有边界情况负责。Lean 厉害在它比绝大多数类型系统更严格但它验证严格性的哲学值得借鉴。5.2 给想复现类似流程的人几条实际建议如果你看了这篇也想用 Claude 或类似模型去碰一碰 Lean下面这些建议来自真实踩坑不要一上来就立 FLT 这种巨型目标。先用自然数和初等数论练手比如证整除性质、同余关系把 Lean 和 Mathlib 的基本 API 摸熟。使用项目模板初始化一个 Lake 工程并把 Mathlib 作为依赖。不要在某个临时文件里全靠手里的模型瞎猜#check是你验证符号是否存在的第一道防线。把模型当成“tactic 生成器”而不是“全知数学家”。让它一次只写一个引理或一个证明块然后立刻执行lean编译不要让它一次性吐出整个巨大theorem。遇到错误信息先看变量的类型和作用域。大量失败不是数学不会而是同一个名字在不同引理里被赋予了不同含义。把大证明拆成容易命名的小引理好的命名能让模型后续调用时更轻松。如果你把所有 helper 都叫lemma1、lemma2上下文一长模型就彻底分不清谁是谁了。最后保持“证明文件能跑通”和“这个证明结构是否优雅”两条线同时推进。不要为了通过验证就无脑把问题拆成一地碎片那样以后维护成本会高到让人崩溃。5.3 这件事对软件验证可能带来的后续影响有了这种“AI 生成 形式化验证”的样板我认为接下来会看到更多基础设施性质的落地场景智能合约的逻辑验证、协议的状态机规范、算法伪代码的可执行规范甚至金融系统里的核心计算逻辑。以前这些领域缺少的不是写规范的人而是缺少一个能把这些规范快速变成验证结果的高效生产者。Claude 在 Lean 里生成的证明代码虽然在数学术语上不一定优雅但它既然能被机械检查就说明至少在逻辑层人类要少操很多心。当然现实距离“完全无人值守的自动形式化证明”还非常远。模型依然需要人类定义目标需要人类审查策略也需要大量底层的数学库支撑。但至少 Anthropic 这次用 11 天告诉我们只要裁判足够冷酷AI 的产出就有机会变得值得信赖。我自己的最终体会是别把“AI 证明数学”看成一场取代人类的竞赛它更像我们终于遇到了一种比“让模型自己说什么是对的”更高级的用法——让模型在“必须达到某个客观标准”的环境里持续尝试、撞墙、重来。Lean 就是那堵诚实又坚硬的墙。你问我想不想尝试一次用 AI 形式化“多项式时间的欧拉回路判定”这类小型定理我的回答是随时都想而且建议你也试一次。踩过两轮错误再回头看这篇 Anthropic 的成果你对“11 天”的理解会比看热榜新闻深得多。