1637 年费马在《算术》拉丁文译本的书页边写下那句著名的批注“我发现了一个真正绝妙的证明但这里空白太小写不下。”他大概率不会想到这句话会让数学家们忙活 357 年更不会想到最后被一个不搞数学的工具“收拾干净”。2025 年年中Anthropic 与斯坦福大学团队公开了一项工作他们让大规模并行的 Claude 实例在 11 天时间里把费马大定理的完整证明形式化到了 Lean 证明助手中得到了所谓的“机器检验证明”。消息一出很多人的第一反应是“AI 会证明数学题了”这理解太浅。真正值得讨论的问题是为什么人类审了几年才算放心的证明机器 11 天就能逐步检验完以及这种“让电脑替你证明数学”的能力和普通开发者写代码有什么关系这篇文章先澄清一个判断再讲清楚机器检验证明到底在验证什么最后用一套可操作的 Lean 4 Claude Code 工具链帮你亲手写出并运行第一个机器可验证的证明。读完你会明白这件事不是数学圈里的花边新闻而是“把人类思路变成机器可执行对象”这个工程范式第一次出现在一座所有人都认识的高峰上。1. 11 天验证费马大定理这件事为什么值得关注先回到问题的起点。怀尔斯在 1994 年给出的费马大定理证明大概是现代数学史上审查强度最高的一篇论文。它依赖椭圆曲线、模形式、伽罗瓦表示、岩泽理论、Hecke 代数等多个艰深分支几百页的内容层层嵌套任何一个环节漏掉一个条件都可能造成整条链断裂。怀尔斯当年甚至公开承认过第一版证明里有漏洞随后又花了几个月补上。这暴露了一个长期存在的结构性尴尬人类数学界对“证明可靠”的判断依赖的是顶级数学家们逐行阅读、反复沟通、彼此说服。这是一个极其昂贵且漫长的社会性审查过程。但数学证明本身应该是一串从公理出发、每一步都可由机械规则检查的推理链。传统论文做不到这一点因为作者默认读者共享大量背景知识许多步骤被压缩成“显然”。所谓机器检验证明就是把那套“显然”全部撕开让计算机从最底层公理开始用类型检查器逐条核对。计算机不“理解”证明它只做一件事检查你构造的证明对象是否符合你声明的定理类型。通过了就是通过不通过就没有讨论余地。这也就是“11 天”最让人震撼的地方。它不是在说 AI 突然推翻了怀尔斯的结论而是说把怀尔斯证明从“人类可读的论文语言”翻译成“机器可核验的 Lean 语言”再让 Lean 逐条确认这个巨大的翻译与验证工程已经可以做到接近工业流水线的程度。Anthropic 团队在自己的公开介绍里也把这个工作描述为“大规模生成加机器验证”的实验拆解成大量小型证明目标用 AI 并行补全再通过 Lean 的自动检查保证正确性。所以这件事真正值得关注的不是数学而是数学工程。而数学工程和软件工程之间并没有一道清晰的分界线。2. 机器检验证明计算机说“通过了”到底是什么意思要理解这个新闻得先弄明白 Lean 是什么以及它和普通编译器、测试框架有什么区别。Lean 是一个证明助手更准确地说是一个基于依赖类型理论的交互式定理证明器。它最早由微软研究院推出目前 Lean 4 是社区主推的版本配合 Mathlib 数学库已经被大量数学系和计算机系研究者使用。在依赖类型理论里“命题”和“类型”是一回事。一个定理的陈述比如“对任意自然数 n有 n 0 n”会被表示成一个类型而“证明”则被表示成这个类型的实例。这种设计的奇妙之处在于计算机检查一个证明不需要理解证明者的思维过程只需要运行一个类型检查算法。如果证明对象的类型和定理陈述的类型匹配证明就是有效的。这比“写完单元测试然后祈祷用例覆盖正确”严格得多也比“让几个数学家开会讨论”可复制得多。有一个类比把这件事说得很清楚普通程序里你写一个函数编译器只检查它是否符合类型签名不检查它是否满足业务逻辑但 Lean 里业务的“业务逻辑”本身也是类型。定理就是函数签名证明就是函数体编译器连业务逻辑一起检查。你可以把 Lean 理解成一种“运行在类型层面的编译器”。那么测试呢测试能证明没有 bug 吗不能。测试只能证明几个样例通过。但 Lean 的机器检验证明一旦被接受就意味着在给定的公理体系和编码约定下这条命题对所有对象都成立不存在“没测到”的边角情况。看到这里你就明白了所谓“机器检验证明”本质上是一种特殊的程序构造。费马大定理的形式化工作等于在 Lean 的数学库里新增了几万个互相咬合的函数和类型。Claude 在其中扮演的角色主要是“把人类论文翻译成这些函数和类型”——翻译、搜索、修错而不是发明新的证明路线。3. 费马大定理为什么难形式化很多人会问既然 Lean 只是“检查”证明那让程序员把怀尔斯的论文翻译成 Lean是不是就是一个体力活真要做会发现根本不是体力活而是地狱难度的软件工程问题。第一层难点是数学对象数量庞大。怀尔斯证明中涉及大量现代数论概念模曲线、Galois 表示、Hecke 代数、岩泽理论、Selmer 群等。你必须在 Lean 里先把这些概念定义出来。每一个概念的定义都会牵涉一长串前置定义。Mathlib 数学库发展多年已经积累了大量基础数论内容但离直接支撑费马大定理还有相当距离。前面提到的团队公开介绍中也强调了他们为了让证明在 Lean 中落地扩充了大量数学库定义和辅助引理。第二层难点是论文中的大量省略步骤。数学家写“由命题 X 显然可得”的时候省略的可能是几十步机械推导。AI 简历里把这句话翻译成 Lean 时需要自行展开成一个合法的证明项。这种展开过程很像重构一段烂代码表面问题很简单拆开之后到处是隐藏依赖。第三层难点是证明本身的拓扑结构。怀尔斯证明不是一个线性列表而是一棵树。不同分支可能使用不同的数学定义体系有的分支依赖于前面的某几条引理有的分支又在末尾统一回汇。AI 并行处理时靠的是任务拆解和结果汇总。某一条引理失败可能让整个子树无法继续必须回溯、调整上下文再重试。正是这最后一点决定了这项工作不像普通人想象中那样“把论文丢给大模型”。在公开的流程描述里这个项目大概是这样运作的先将怀尔斯证明拆成数量庞大、粒度均匀的子目标每个子目标都由一个 Claude 实例独立或接力处理处理过程中模型会参考已有 Mathlib 定义、论文文本的局部段落、其他子目标产出的引理每次生成的结果都会立刻交给 Lean 编译器检查检查失败就根据错误信息修正最终所有子目标通过后整个证明由 Lean 自动验证一遍。所以那 11 天不是“模型思考了 11 天”而是“几千台并行的 AI 进程在 Lean 的反馈回路里修修正正跑了 11 天”。4. Claude 是怎么参与的从非形式证明到 Lean 证明如果只看新闻标题很多人会误以为 Claude 真的“独自证出了费马大定理”。这是最需要纠偏的地方。怀尔斯证明的核心数学思想仍然属于怀尔斯。Claude 做的事情是整个项目中段和后段的“翻译加工程化验证”把人类可读的证明变成 Lean 可执行的证明文件。这里可以拆成几个具体环节。第一个环节是拆解。一个大型定理的证明先被切分成大量独立子目标。怀尔斯证明的章节结构本身就有天然的分界某个引理用于证明某类伽罗瓦表示的形变理论某个命题又用于连接模形式与椭圆曲线。团队需要把这些分界手工标注清楚形成任务清单。这一环节目前还非常依赖人类专家因为哪些内容需要先定义、哪些结论可以在 Mathlib 中找到必须对数学内容有很深理解。第二个环节是生成。每个子目标交给 Claude 时不是只给一句“请证明 XX”。模型需要读取论文中对应的段落了解目标上下文还要能查询 Mathlib 中已有的定义、定理和记号。这和平时用 Claude Code 写业务代码很像你的工作区里有仓库、有依赖、有报错信息AI 会结合这些上下文输出候选代码。第三个环节是检查与修复。这是整个流程中最像“软件工程”的部分。Claude 生成一段 Lean 代码后Lean 编译器返回结果要么通过要么带着类型不匹配、未知标识符、目标未闭合等错误信息拒绝。Claude 看到错误后修正再提交再检查。这个过程本质上是“AI 写代码 编译器做 CI”的循环只不过这里的 CI 极其严格不是跑几个测试用例而是直接做形式化验证。第四个环节是汇总验证。所有子目标通过后整个证明项目要在 Lean 中统一构建。任何一个子目标伪造了定义或者依赖了未被允许的假设都会在这一步暴露。从这些环节可以看出Claude 在这 11 天里的角色更像是“一个极其有耐心的菜鸟程序员”而不是什么数学天才。它真正的优势是三点并行数量大、失败后不气馁、每次修正都基于编译器的真实错误信息。这三个优势加在一起才把过去多年都无法完成的形式化工程压缩进了两周。这里还要强调一个边界判断这是一个工程成就不是新的数学发现。它没有改变费马大定理证明本身的数学结构也不是要替代数学家去发现新定理。它的意义在于把“人类认为正确的证明”升级成了“机器可以独立检查正确的证明”为后续的数学出版、论文评审、软件安全验证提供了一种新的基础设施。5. 从零开始Lean 4 环境搭建与基础配置前面讲了一堆概念接下来进入动手环节。这一节先把 Lean 4 环境搭起来。版本细节建议以官方仓库最新说明为准这里重点演示通用思路。5.1 安装 Lean 4Lean 4 官方推荐通过 elan 安装。它是一个类似 rustup 的版本管理工具可以在不同项目间切换 Lean 版本。在 macOS 和 Linux 上常见的安装命令是curl -fsSL https://elan.lean-lang.org/lean-installer | shWindows 用户更推荐使用官方提供的安装脚本或者直接在 WSL 里操作。执行完脚本后重新打开终端让环境变量生效。随后设置默认工具链elan default stable验证是否安装成功lean --version lake --version如果能正常输出版本号Lean 4 和构建工具 lake 就都已经准备好了。5.2 安装 VS Code 扩展Lean 4 最常见的使用方式是在 VS Code 里编辑 .lean 文件。打开扩展面板搜索“Lean4”安装由 Lean 社区维护的官方扩展。安装完成后打开任意 .lean 文件VS Code 会自动调用 lean-language-server。如果你更喜欢 Neovim社区也有对应的 Lean 插件但本文不展开。实际项目中VS Code 的体验足够稳定也最容易排查问题。5.3 创建 Lean 项目Lean 项目使用 lake 管理。先新建项目目录lake new demo cd demo这个命令会生成一个标准项目结构包含 lakefile.lean、Main.lean 等文件。新建一个实验文件 Demo.leantouch Demo.lean后续的小节会在这个文件里写 Lean 证明。需要注意的是如果要用到 Mathlib 数学库需要在 lakefile.lean 中声明依赖然后执行lake update再执行lake build来下载并编译。Mathlib 很大首次构建会非常耗时建议在网速好的环境执行。本文的核心示例尽量不依赖 Mathlib避免读者卡在漫长的编译步骤上。6. 用 Claude Code 协助编写第一个机器检验证明现在进入最实用的一节怎么把 Claude Code 变成你的“形式化数学助手”。6.1 安装 Claude CodeClaude Code 是 Anthropic 推出的命令行编程助手它可以直接在你的终端里读文件、跑命令、看报错然后生成代码或修复代码。安装方式依赖 Node.js 环境先确认你的终端已经安装 Node.js 18 以上版本。安装命令npm install -g anthropic-ai/claude-code安装完成后进入项目目录运行claude首次运行会让你登录或配置 API 密钥。如果选择使用 API 方式需要在环境中配置 ANTHROPIC_API_KEYexport ANTHROPIC_API_KEYsk-ant-xxxx注意这里不要真的把密钥写进代码库更不要提交到 Git。推荐使用系统环境变量或密钥管理工具避免泄露。在 Windows PowerShell 中如果出现“claude 不是内部或外部命令”的提示通常是因为 npm 的全局 bin 目录没有加入 PATH。可以先启动一个新的终端窗口若仍然无效临时使用npx anthropic-ai/claude-code这种方式不依赖全局 PATH适合快速临时使用。6.2 编写并验证一个归纳证明先写一个最经典的 Lean 证明对任意自然数 n有 n 0 n。虽然这个结论在现代数学库中是内建引理但手工证明一遍能让你立刻感受到“证明即程序”的意思。在 Demo.lean 中加入以下内容-- 文件路径demo/Demo.lean -- 证明对任意自然数 n有 n 0 n theorem add_zero_example (n : Nat) : n 0 n : by induction n with | zero rfl | succ n ih calc Nat.succ n 0 Nat.succ (n 0) : rfl _ Nat.succ n : by rw [ih]逐行解释一下induction n with触发对自然数 n 的数学归纳。zero分支对应 n 0。此时要证明0 0 0这在定义层面就直接成立所以用rfl解决。succ n ih分支对应 n 的后继。ih是归纳假设内容正是n 0 n。在calc中第一步Nat.succ n 0 Nat.succ (n 0)是加法定义直接展开可以用rfl闭合第二步用rw [ih]把归纳假设套进去得到最终目标。运行验证命令lake env lean Demo.lean如果文件没有类型错误命令不会输出任何内容直接静默结束。这就是 Lean 最典型的“成功方式”。如果你看到一个空终端说明证明已经通过。再用 Claude Code 做同样的事。在终端运行claude -p 请用 Lean 4 证明对任意自然数 n有 n 0 n。给出完整代码。Claude 会返回一段类似上面那样的 Lean 代码。你把它放进 Demo.lean再运行同一句lake env lean Demo.lean验证即可。这里最关键的工作方法是AI 给你代码最终验证权始终在 Lean 编译器手里。6.3 让 Lean 拒绝一个错误证明为了体会“机器检查”的严格性再看一个反例。在 Broken.lean 中写-- 文件路径demo/Broken.lean -- 这是一个故意写错的证明 theorem broken_one : (1 : Nat) 2 : by rfl运行lake env lean Broken.lean正常来说Lean 会立刻报出类型不匹配错误因为它发现1和2在定义层面并不相等。这就是机器检验证明和传统论文“专家审核”之间的本质差异它不会因为 1 和 2 看起来差不多就放行。让你写的这个错误证明成为你的第一个调试案例。此时打开 Claude Code把报错信息贴给它说“帮我修复这个 Lean 错误”。理论上它会把错误原因解释清楚并给出的结论是“这个命题无法证明”。不要觉得好笑这个交互过程恰恰是大规模费马大定理项目中无数个小型修复循环的缩影。7. 常见问题与排查思路自己动手时最容易踩到的坑往往集中在环境安装和 Lean 语法上。下面整理的排查表基本覆盖了最常见场景。问题现象可能原因排查方式解决方案claude 无法识别为 cmdlet、函数或可运行程序npm 全局 bin 目录未加入 PATH或安装中断新开终端后重新运行claude --version在 Windows 上检查 PATH把 npm 全局目录加入 PATH临时用npx anthropic-ai/claude-code代替报错 error: claude native binary not installednpm postinstall 脚本未执行或安装包损坏重新执行全局安装命令查看 npm 日志npm install -g anthropic-ai/claude-codelatest必要时完全卸载后重装Lean 文件打开后提示 unknown identifier.lean 文件不在 lake 项目中或项目未初始化确认目录结构查看是否有 lakefile.lean用lake new创建项目进入项目目录后再执行lake env lean运行lake env lean报依赖错误项目中依赖的包未下载查看 lake-manifest.json 是否存在执行lake update后重新构建Mathlib 编译时间太长数学库体量巨大首轮构建需要编译全部内容观察终端是否仍在输出编译日志耐心等待若网络受限考虑科学配置镜像源或先用本文不依赖 Mathlib 的示例Lean 报 type mismatch 或 tactic failed证明步骤与目标不完全匹配使用#check和#print检查当前状态拆解证明步骤用exact或rw逐步闭合目标Claude Code 生成的 Lean 代码无法通过编译AI 对 API 或库版本的记忆过时把完整报错信息给 Claude并要求它只基于当前报错修正让 Claude 读取当前文件和工作区后重新生成不要求它凭空想象这里重点说一个新手最容易忽略的习惯运行 Lean 文件的命令一定要在项目根目录下执行。如果你随便在临时目录建了一个 .lean 文件然后执行lean Demo.lean很可能因为找不到 Mathlib 或项目配置而报错。规范动作是先在项目目录下用lake env lean 文件名执行。8. 最佳实践与工程建议如果看完前面的内容你准备在自己的项目里把“AI 辅助形式化验证”用起来这几点建议应该能帮你少走弯路。第一从引理而不是定理开始。费马大定理的形式化项目之所以能成功很重要的一点是把证明拆成了大量独立的、粒度均匀的小目标。你在自己的项目里也一样不要上来就让 AI 证明一个五层嵌套的复杂结论。先把最内层的小引理喂给 AI验证通过后再一步步向上组合。第二把编译器当作唯一裁判。这个原则再怎么强调都不过分。AI 生成的证明看起来合理甚至和你阅读论文得到的印象一致但只要 Lean 报 type mismatch它就是错的。不要试图“说服”编译器也不要不看报错就反复让 AI 重试。正确的做法是把报错原文交给 AI让它基于报错修正。第三固定工具链版本。Lean 4 和 Mathlib 都处于快速演进阶段。今天能通过的证明三个月后因为 Mathlib 重构可能就过不了。实际工程里务必把 lake-manifest.json、lean-toolchain 等版本描述文件提交到 Git。团队协作时所有人的 Lean 版本必须保持一致否则会出现“在我电脑上能跑”的经典问题。第四用 CI 守护证明。你的证明项目如果会长期维护建议在 CI 里加入lake build或lake env lean命令让每一次提交都自动验证所有证明。这和软件项目里用 CI 跑测试是一样的。想想看当证明数量多到几千个时人工排查哪一个被改坏是不可接受的。第五注意模型上下文长度。Claude 处理单个证明任务时上下文窗口是有限制的。如果某个子任务太大建议拆成更小的中间引理分多次发送。这和把大函数拆成小函数的好处一样模型更容易理解局部目标编译器也更容易定位错误。第六安全与权限问题。在团队环境中使用 Claude Code 时务必明确它是否可以执行任意终端命令。Claude Code 的设计允许它读取文件、运行命令这是方便也是风险。建议在自己掌控的开发环境里使用不要在未获得授权的生产环境随便执行它生成的删除、修改或批量操作指令。涉及数据库删除、系统级配置变更等操作必须有备份和回滚方案。第七机器检验证明并不等同数学真理。这一点需要给所有人的脑子都泼一盆冷水Lean 只能验证“在给定公理与给定编码下证明是有效的”。它不能保证你一定没有把数学概念编码错误也不能保证你选择的公理体系本身不矛盾。查阅一个大型形式化项目除了看最后有没有全部通过还要看它的定义是否忠实于目标数学概念。这也是为什么人类数学家依然很重要。9. 未来可做的事费马大定理的机器检验证明给技术圈带来的最直接启发不是什么“数学家要失业了”而是一个判断过去被认为需要“专家品味”才能完成的复杂形式化工程现在可以用“拆解加 AI 加机器检查”的方式大规模推进。这个模式完全可以平移到更贴近软件工程的地方比如协议验证、安全审计、智能合约正确性证明等。如果你想沿着这条路继续深入建议下一步按这个顺序走一遍先把今天 Demo.lean 里那个归纳证明完整读通做到不看答案自己敲出来。然后去 Lean 官方教程里学习rw、simp、exact、calc这几个最常用的证明策略。等你在 Lean 里证明过二三十个小引理后再回头看看 Claude Code 能不能协助你证明一个更复杂的小定理比如整数加法的交换律。到这一步你已经不是“在看 AI 证明费马大定理”的围观群众而是真正体验过这条流水线的参与者了。工具链已经摆在这里Lean 是免费的Claude Code 也有现成的安装方式连整个证明过程的思路都公开了。剩下的只是打开终端跑通第一个rfl。