说个刚刷屏形式化验证社区的消息Claude 辅助完成了费马大定理的首个全机器校验形式化证明。注意这里的措辞不是“AI 独立证明了费马大定理”而是“在 AI 辅助下怀尔斯的证明被完整翻译成了机器可验证的 Lean 语言并且全机器校验通过”。这两者的差别恰恰是理解这次事件价值的关键。费马大定理是什么一句话当 n 大于 2 时方程 x^n y^n z^n 没有正整数解。这个猜想 1637 年由费马提出直到 1994 年才被安德鲁·怀尔斯用一套极其庞大的现代数学工具证明。而所谓“形式化证明”是把证明的每一步都翻译成形式语言的推理规则最终由机器内核逐条验证。以前这件事被认为是人力几乎不可能完成的因为怀尔斯的证明跨度太大、依赖的分支太多。这次突破等于在数学和计算机科学之间架了一座桥一座完全由机器验收的桥。这篇文章不打算只讲故事我想带着大家从四个角度把这件事彻底拆开费马大定理形式化到底难在哪从怀尔斯原证明到 Lean 可验证代码的技术链路是什么Claude 在这场工作中到底扮演了什么角色以及如果你自己也想用 Claude Code 和 Lean 做类似的事实操上应该怎么配置、怎么写策略——这部分我踩了不少坑会一并交代。1. 费马大定理形式化的难点——为什么等了这么多年才等到这一天1.1 费马大定理在数学史上的分量先给不熟悉的读者补个背景。费马大定理不是一般的高考压轴题它是“民科重灾区”和“数学界试金石”。费马本人 1637 年在《算术》一书的页边写下这段猜想还留下一句著名的“我确信已发现一种绝妙的证明可惜空白太小写不下”。后来的事大家都知道了此后三百多年无数数学家试图证明欧拉证明了 n3 的情况索菲·热尔曼处理了一类素数库默尔提出了理想数理论——这些努力催生了代数数论这一整个分支但完整证明迟迟没有出现。直到 1994 年安德鲁·怀尔斯才给出了完整的证明。这版证明有多“重”它建立在模形式、椭圆曲线、伽罗瓦表示、岩泽理论、变形环等多个当代数学分支之上完整证明有上百页后来经过一个补丁修正才彻底过关。换句话说怀尔斯不是灵感一现而是把二十世纪后半叶最前沿的数学工具全用上了。这带来一个直接后果如果你想把怀尔斯的证明做形式化你不能只形式化“一个定理”你得先把这串证明所依赖的庞大数学大厦一块砖一块砖地搬进去。这就像你要用乐高搭出一个完整的埃菲尔铁塔但你得先拥有足够的梁、柱、铆钉而且每一颗铆钉都要经过同一套标准检验。1.2 “机器校验的形式化证明”到底在验证什么很多人第一次听到“形式化证明”会误以为这是“计算机帮我们把证明过程检查一遍”。这个理解方向对但标准要严得多。手写论文的“检查”依赖数学家的共识和直觉可能有盲区而形式化证明是把证明写进一个约束极其严格的形式语言比如 Lean、Coq、Isabelle机器内核会按逻辑规则一步步推导任何一步如果引理没用对、类型对不上、条件不满足就会被拒。可以这样理解手写证明像是你提交一篇论文编辑找几位同行评审大家认为逻辑没问题就发了形式化证明则像是把论文里的每个运算步骤都写成一个程序交给编译器逐行检查语法错、类型错、逻辑断点全部直接编译失败。前者靠智识权威背书后者靠机器的机械确定性。费马大定理这种长度的证明形式化的难点不只是“篇幅大”更致命的是“分支多”。怀尔斯证明里用到的数学对象分散在代数、数论、几何好几个领域而且彼此之间有很多高层级的抽象。你要是只形式化其中一条引理链那不难难的是把整座大厦的所有承重结构统一建模还得保证不同模块之间的接口严丝合缝。1.3 为什么以前没人做出来其实 Lean 社区一直在推进费马大定理的形式化项目这件事不是一夜之间发生的。形式上它需要两个前提一是有一个足够强大的证明助手和数学库二是有一批既懂数学又懂形式化的工程师。前者在 Lean 数学库 Mathlib 逐渐成熟后才具备后者更是稀缺。这里要提一个大家容易忽略的现实怀尔斯证明中有些步骤原始论文里写得也不是特别详细部分依赖前人论文的结论。做形式化时你得把这些“隐藏依赖”也全部补出来。这不只是翻译工作有时候等于重新做一遍研究因为你必须弄清楚某个断言到底从哪里来、靠什么定理保证。这个成本在很长一段时间内是人类数学家不太愿意投入的。所以这次事件的核心意义之一是 AI 把这个巨大工程中的很多“脏活累活”接下来了让一个原本可能要耗费数十人年级别的工程在可接受的时间窗口内跑通了。这才叫真正的“全机器校验”。2. 从怀尔斯手写证明到 Lean 可验证代码的技术链路2.1 为什么最终落在 Lean 上市面上的证明助手不止一个最常见的还有 Coq、Isabelle、Agda。为什么这次事件的主角是 Lean 而不是别的一个直接原因是数学库 Mathlib 的积累。简单打个比方你要盖一栋摩天大楼Coq 给你的是一套很好的钢筋混凝土规范但钢筋得自己生产Lean 的 Mathlib 则是已经帮你预制好了大量的梁、板、柱你直接调用即可。Mathlib 在过去几年里把本科到研究生阶段的大量数学结论形式化了包括代数、拓扑、分析、数论等多个领域。怀尔斯证明里需要的一些现代代数几何基础Mathlib 里已经有相当一部分实现。下表是我个人对各主流证明助手在“数学全库建设”上的印象对比证明助手数学库成熟度自动化程度适合场景Lean 4很高Mathlib 覆盖广高有 linarith、omega、simp 等自动化策略纯数学、大工程证明Coq较高但库的覆盖面偏程序验证中高更适合程序语义、编译验证程序验证、函数式编程Isabelle/HOL高但不同领域自成体系高有 sledgehammer 等多种自动工具逻辑、程序验证从这个角度你会发现Lean 在“纯粹数学的大规模形式化”这个目标上天然有优势。费马大定理这种级别的证明依赖的不是某一两个孤立的定理而是横跨数论、代数几何的成建制理论体系Mathlib 正好提供了这种体系。2.2 把怀尔斯证明拆解成可处理的任务形式化怀尔斯证明不是把 PDF 扔给机器就能自动读懂的。实际项目里的人做法是先把整个证明拆成一个“定理树”根是费马大定理下面是支撑它的若干大定理比如“所有半稳定椭圆曲线都是模的”怀尔斯证明的核心即费马大定理的重要推论再往下是支撑这个大定理的各种引理和定义。每一层都可以在 Lean 里声明成theorem或lemma然后逐个去证明。代码层面大概长这样theorem fermat_last_theorem {a b c : ℕ} {n : ℕ} (hn : 2 n) (hpos : a 0 ∧ b 0 ∧ c 0) (h : a^n b^n c^n) : False : by -- 这里通过调用 frey 曲线、模性定理等多个大引理来完成证明 exact modularity_fermat hn hpos h当然这只是示意真正的证明远比这个复杂。但关键是每个theorem在 Lean 里都是一个“待验证的目标”每一次验证都由内核执行。只要有一个引理没证明整个工程就完不成。2.3 Claude 在证明补全和策略生成上的作用人类在做这种大规模形式化时最多的精力往往花在“策略搜索”上。Lean 的证明过程是写“策略脚本”比如rw、simp、linarith、apply这些指令告诉机器下一步怎么推导。很多时候你面对一个目标并不知道该用哪个策略、该补哪个引理。这一步很像程序员调代码看到报错信息理解它然后修正。Claude 做的事情就是把“看到目标、生成策略、验证是否通过”这个循环自动化。它可以读当前的 Lean 证明状态生成接下来的策略代码跑通了就留下跑不通就换一种思路。对于大量重复性、模块化的证明义务这种能力非常管用。我还看到一些项目里用 Claude 做“缺口分析”给出一个大定理的陈述后让模型判断手里有哪些引理哪些中间结论还缺着然后自动补充证明。这个能力放以前需要人类数学家花很长时间梳理文献才能做到。2.4 “通过校验”究竟意味着什么最后这句话必须说清楚“全机器校验通过”不是说 AI 或人类觉得证明没问题而是 Lean 的内核接受了整个证明文件。Lean 内核非常小只负责约简、类型检查、替换等一组基本规则所有高层定理最终都要归约到这些规则上。这意味着证明的可靠程度已经不在“专家认为正确”这个层面而在“逻辑规则推演结果”的层面。内核级验证还有一个好处它降低了读者对论文的信任成本。以后任何人要确认怀尔斯证明是否成立不再需要重新读完全部证明笔记、核对所有引理打开机器校验过的形式化文件跑一遍编译器通过就是通过没通过就是没通过。这对数学界的知识传播方式是一个很深的改变。3. Claude 在形式化里的真实角色更像“证明工程师”而不是“数学家”3.1 不要把 AI 辅助误解成 AI 独立发现我看到不少媒体标题写得很夸张好像 Claude 一夜之间成了推翻数学界的“机器天才”。实际不是这样。怀尔斯证明的核心洞见——把费马大定理与椭圆曲线模性定理联系起来——是人类数学家用几十年时间构建出来的。AI 在这件事里更像是一个极有耐心的“证明工程师”它不负责提出宏大猜想但负责把宏大猜想变成一行行机器认可的代码遇到断点就尝试修补最终让整条链路闭环。打个比方一位建筑大师画出了摩天大楼的完整设计图以前只有一支精干的施工队才能把图纸变成现实现在来了个不知疲倦的机器人团队建筑还是那个建筑但施工速度和容错能力完全不同。Claude 不会新增建筑学知识但它让“把图纸变成建筑”这件事变得可行。3.2 AI 在证明链路中的三个具体贡献我在拆解各个项目的公开材料后总结了 AI 在里面的三种典型作用策略生成与补全面对一个 proof goal生成simp、rw、induction、linarith等策略序列或补上缺失的中间引理。代码翻译与转写把论文中自然语言写的数学结构群、环、模、层转成 Lean 的定义和定理陈述。这一环对语言理解能力要求很高也是大模型最擅长的地方。批量处理重复性证明义务在大型形式化工程里会有大量结构类似的“边角证明”比如“加上这个条件后原来的证明套路依然成立”。AI 可以在人类给定模板后批量生成变体证明极大解放人力。这三点都不是“发现新数学”但正是这些工作占据了过去团队 80% 的精力。把这块成本降下来形式化工程的进度自然就上去了。3.3 人机分工的新范式这次里程碑最有借鉴意义的地方在于人机分工的范式人类负责“战略控制”AI 负责“战术展开”。人类提出整体证明框架、拆分定理树、确定关键引理AI 负责在既定路径上生成具体策略、补细节、查缺口。两者不是替代关系而是上下级协作关系。我更愿意把这种模式称为“证明军队里的参谋部加士官班底”参谋长规划战役方向士官负责把每个阵地的战斗打下来。Claude 是那个特别能打的士官但它不能替代参谋部的战略判断。4. Claude Code 配上 Lean 的实操记录环境、策略、避坑这部分写给被热搜词勾过来、想亲手试试“AI 辅助形式化证明”的操作党。我默认你有一点 Lean 4 基础没基础也没关系照着步骤来先跑通一个最小例子后面再慢慢深入。4.1 为什么我用 Claude Code 而不是网页版聊天网页版 Claude 适合问答型交互但形式化证明是典型的“迭代式工作流”你打开一个 Lean 文件编译报错改策略再编译。如果每次都把当前文件内容复制粘贴到网页对话框再把返回的代码粘回文件效率太低而且容易漏掉上下文。Claude Code 是 Anthropic 提供的命令行 Agent 工具它能直接读取项目目录下的文件、执行命令、查看编译输出然后自己修改代码。这个“读文件-跑命令-看结果-改文件”的闭环正是证明工作时最需要的。它和 Lean 的结合特别自然Lean 编译器报错后Claude Code 可以直接拿到错误信息并尝试修复。在 VS Code 里我通常是把 Lean 文件和一个终端并排放置。左侧跑 Lean 的语言服务器右侧跑 Claude Code。需要补证明时直接把目标定理描述给 Claude Code它会返回一段 Lean 策略代码复制到文件里再编译验证。这套流程我已经用了很久稳定程度远超手动复制粘贴。4.2 环境准备与配置要点先列一个我验证过的最小环境组合Lean 4建议直接装最新稳定版。Mathlib4用lake管理项目时默认会拉取已声明的 mathlib 依赖。VS Code Lean 扩展主要是为了交互式编译在鼠标悬停时查看每个 proof state 的变化。Claude Code需要 Node.js 运行环境然后用 npm 全局安装anthropic-ai/claude-code。在 VS Code 集成时你还要做一件事让 Claude Code 能调用lake env lean或lake build。简单说就是在 Claude Code 里告诉它当前项目用的是什么编译命令它在改完代码后自己去重新编译。这一步如果漏掉Claude 就只能“盲写”——服务端大模型并不知道 Lean 编译器返回什么错误效果会差很多。安装完跑一下帮助命令确认环境正常claude --version我个人踩过的一个坑Windows 上经常报“无法将‘claude’项识别为 cmdlet、函数、脚本文件或可运行程序的名称”原因通常是 Node.js 的全局 bin 目录没加入 PATH。把%APPDATA%\npm加进系统环境变量重开终端即可。4.3 一个能跑通的最小示范自然数加法结合律先别一上来就碰费马大定理直接起步就该从小目标开始。我最常用的练习是证明自然数加法结合律import Mathlib.Data.Nat.Basic theorem add_assoc_example (a b c : ℕ) : (a b) c a (b c) : by induction a with | zero simp | succ a ih simp [ih]把这段代码交给 Claude Code 时我会给这样的提示请在 Lean 4 中证明自然数加法结合律注意用的是 Mathlib不需要自己定义加法直接用库里的定义。我的环境是 Lean 4 稳定版。请返回完整的 theorem 代码并说明你用了哪些策略。Claude Code 会返回类似的策略脚本。把它写进.lean文件保存后 Lean 语言服务器会立刻编译。如果通过会在 VS Code 里看到没有任何红色波浪线。这一步虽然简单但能把整个工具链验证一遍。4.4 让 Claude Code 更省 token、更准的实用技巧热词里频繁出现“claude code 如何用省 token”这个问题实际操作中确实值得重视。形式化证明任务里文件传输和编译错误信息都会吞掉大量上下文。我的做法是给 Claude Code 交代“工作边界”让它只管当前这个定理相关的部分不要整个项目扫一遍。具体提示词我一般写成这样说明文件范围当前工作目录下只允许修改Test.lean不要动其他文件。说明目标补全add_assoc_example的 proof不要新增其他定理。说明输出格式只输出最终可编译通过的完整 Lean 代码附简短解释不要写长篇大论。说明失败处理如果编译报错把错误信息贴给我等第二次指令再动手。这样一套约束下来上下文使用量能比默认模式省一半以上而且返回内容更可用。有一点要特别注意大模型有时会自信地“编”出不存在或错误命名的引理。解决办法是让它先用#check验证潜在引理的存在性再写进证明。比如#check Nat.add_assoc如果这行能在 Lean 里编译通过说明引理确实存在。这条小习惯能帮你避开大量“假引理”问题。4.5 常见报错与排查清单我在实操中总结了一张常见问题表按出现频率排序报错或现象原因解决办法unknown identifier引理名拼错或对应库未导入用#check验证或搜索 Mathlib 里的实际命名type mismatch目标类型和引理签名对不上检查元组、括号、隐式参数必要时用show显式转换类型failed to synthesize instance缺少某个类型类实例确认已经 import 相应的数学结构定义unsolved goals策略没完全处理掉所有目标分支把 proof state 发给 Claude Code让它补充剩余策略Windows 下 claude 命令不存在npm 全局 bin 不在 PATH 中把%APPDATA%\npm加入系统 PATH重开终端另有一个非常隐蔽的坑Lean 4 不同版本的库 API 有差异。你在网上搜到的一个定理名在你本地的 Mathlib 版本里可能已经改名了。遇到unknown identifier时先检查本地 Mathlib 版本和网上教程是否一致。这个排查过程我经历过太多次几乎都指向同一结论版本对齐比写证明本身更容易出问题。5. 这次里程碑的真实边界与下一步5.1 它改变了什么这件事最直接的意义是把“AI 能不能真正参与严肃数学验证”这个问题的答案从“理论可行”变成了“工程已验证”。以前说 AI 能辅助数学大多是猜的数字、猜的路径这次是项级难度的数学成果从手写证明到机器可控的全流程验证AI 真的在里面出了力。第二个改变和“智能体安全”有点关系。形式化验证的核心思想是“对行为给出可证明的保证”这和当下 AI 安全领域的诉求高度同频。如果未来想让所有智能体都遵守行为规范那么“把规范形式化、把行为验证放在内核里”就是一条不得不走的路。这次费马大定理的验证本身虽然和智能体安全没有直接关系但它证明了“全机器校验”在庞大的逻辑链条上是可行的这个信心意义不容小觑。第三个改变是带动了形式化证明的工具链生态。一次顶难里程碑跑通之后Mathlib 里很多原本缺失的模块会被补齐之后做类似证明的起点会更高。这就像修路第一段最难修通了后面的车就都能上来。5.2 它没有改变什么Claude 没有独立发现怀尔斯那样的新证明结构也没有证明出新的未解难题。它没有“灵光一现”也没有“认识论突破”。它做的是在人类给出的框架内把包含大量中间结论的逻辑链路精确落地。这个区别要是含糊过去很容易把这件事误解成“AI 要取代数学家了”那是讲故事不是讲事实。另一个没变的事实是数学突破仍然依赖概念层面的洞察。费马大定理的证明之所以成为传奇不是因为证明过程长而是因为建立了一个根本没人想到过的关联费马大定理的反例能构造出一条椭圆曲线而这条曲线的模性性质最终矛盾了。这种关联属于数学发现不属于形式化工具链的范畴。AI 要能在“发现关联”这个层面做出同等贡献还需要走很长的路。5.3 如果你也想参与这个方向不用觉得自己必须“懂所有现代数论”才能碰形式化证明。说实话更大机会在于交叉能力你只要既懂一点数学、又懂一点工程就可以在形式化社区里找到大量能贡献的任务。Lean 的 Mathlib 里永远有“缺证明”的定理你不需要从费马大定理开始哪怕是从一个代数引理、一个分析结论开始也是为这座大厦添砖。我的建议路径是先在本地搭好 Lean 4 Mathlib 环境然后找几个简单的练习题跑通再用 Claude Code 帮你自动生成、修整证明代码。等熟悉了策略脚本的写作方式再尝试给 Mathlib 提 PR补一两个别人没完成的引理。整个流程逐级递进比直接读大部头理论有效得多。说回这次的费马大定理形式化证明我个人的看法是它不是“AI 统治数学”的信号反而更像是“AI 成为数学基础建设中可靠伴侣”的样板。数学知识里有一大类并不是靠天才瞬间点亮、而是靠逐层地基堆起来的部分过去这类工作最消耗人力现在恰好是大模型最能发挥的地方。最后分享一个我在实操中形成的习惯遇到难缠的证明目标我从不直接问 Claude“怎么证明”而是先把#check相关的引理名全部验证一遍再把当前阶段的目标和已知条件尽可能完整地贴给它。这一步看似笨但能把不存在的引理、错误的类型匹配这类幻觉问题提前掐死在源头。形式化证明的世界里机器比人更喜欢“诚实”——它不会因为你说得漂亮就放过一个类型错误。