前阵子数学圈和程序语言圈被一条消息刷屏Fermat 大定理完成了首个全机器校验的形式化证明而这次的主角不是某个数学教授是 AI 模型 Claude 配合 Lean 定理证明器一步步把证明代码写完、核对完。干这行的人都明白这事和“AI 写个网页、修个 bug”完全不是一个量级——费马大定理从 1994 年 Andrew Wiles 给出经典证明到今天中间隔了三十年把证明拆成机器能理解的逻辑链条工作量大到一度被认为是几十年后的工程。我大概从 2024 年底就开始用 Claude 辅助写 Lean 证明当时还只是拿它做点群论、线性代数的小 lemma没想到这么快就有人把整条费马大定理的证明链路跑通了。写这篇文章是想把这件事掰开揉碎讲清楚它到底证明了什么Claude 在这里面扮演什么角色普通人怎么复现这个工作流以及它对我们写代码、做软件验证的方式会带来什么改变。不管你是搞数学的还是写业务的这一轮机器校验浪潮都值得提前看一眼。1. 这到底是一个什么级别的成果从费马大定理到机器校验1.1 先回顾一下费马大定理本身费马大定理的内容特别简单初中生就能读懂当整数 n 大于 2 时方程 x^n y^n z^n 没有正整数解。费马在 1637 年前后把这个猜想写在丢番图《算术》一书的页边空白处还加了一句“我有一个绝妙的证明但空白太小写不下”。结果这一“空白太小”就让数学家等了三百年。二十世纪各路数学家为它发展出了大量工具最关键的突破来自 Gerhard Frey、Jean-Pierre Serre 和 Ken Ribet 的工作费马大定理被等价转换成“如果存在反例就能构造出一个不满足模性定理的椭圆曲线”也就是所谓的 Frey 曲线。Andrew Wiles 在 1994 年证明了“半稳定椭圆曲线都是模的”顺带把费马大定理拿下了他的证明原稿超过一百页核验工作由多位专家持续多年才完成。严格说 Wiles 证明的是谷山—志村—Weil 猜想在特殊情形下的版本它和费马大定理之间的关系本身就是两步扎实的数学推导先由反例造出 Frey 曲线再证明这条曲线不能是模的从而和模性定理矛盾。1.2 形式化证明与传统数学证明的本质区别传统数学证明追求的是“说服人”只要同行评审觉得逻辑没问题、里面的引理引用没错就被接受。问题在于人脑会累、会跳步、会有默契的惯例。费马大定理完整证明有上千个引理依赖任何一个引理错了最终结论就可能站在沙地上。形式化证明则换了一种玩法把数学命题写进一个像 Lean 的依赖类型论系统里证明步骤必须逐条调用推理规则机器会检查每个步骤是否合法。这等于把证明从“讲给人听”改成“写给编译器看”。在 Lean 里写一个命题“存在某个 n 使得 x^n y^n z^n 成立”本身就是一项类型构造证明过程就是构造一个和该命题类型对应的实例。一旦#check或theorem被接受你可以相信定理成立因为每一步逻辑都被机器验证过。类比来说传统证明像手工写了 100 页 SQL 查询逻辑靠人肉 Review形式化证明像是把整个逻辑写成类型安全代码再交给编译器强制类型检查。无聊但可靠。费马大定理的机器校验就是把 Wiles 证明中所有核心引理的逻辑连接全部搬到了 Lean 中确保没有隐藏假设、没有跳步、没有“显然”。1.3 为什么这件事价值巨大机器校验有三层价值。第一是对数学本身一个经过了 Lean 全量验证的三百年大定理理论上不再有“万一这里还有个隐藏 bug”的阴云证明从“令人信服”升级为“逻辑上必须如此”。第二是对数学工具链做这件事的过程中需要把代数几何、模形式、伽罗瓦表示等多个分支的知识库系统化写进 Lean 的 Mathlib这些沉淀下来的代码以后做别的数论项目都能复用。第三这件事最让我兴奋的是它展示了一条“AI 辅助深度推理”的可行路径Claude 不是简单搜一个已有证明粘贴过来而是要在 Lean 环境里不断尝试、被错误信息打回、再调整策略像人一样逐步逼近正确证明。2. 核心数学与工具链复现所需的基础逻辑2.1 关键数学结构椭圆曲线、模形式、伽罗瓦表示外行看费马大定理的证明流程容易一头雾水我先用最通俗的说法把骨干搭出来。整个证明的核心逻辑是三段式假设费马大定理不成立存在正整数 a、b、c 满足 a^p b^p c^p其中 p 是奇素数。由这组反例构造一条 Frey 椭圆曲线 E这条曲线的判别式、导子都和反例的素数因子挂钩。根据 Ribet 定理这条曲线如果是半稳定的且具有某些局部性质就不可能支持一个 level 为 2 的模形式也就是说它不可能是模的。但 Wiles 证明所有半稳定椭圆曲线都是模的于是矛盾。看懂这个框架后你就会发现形式化证明要处理的不是“一句哲学”而是整个体系里的所有前置引理。包括类域论、形变环理论、Hecke 代数、Iwasawa 理论等等。写形式化证明时不可能绕开这些概念单纯去读 Wiles 的一百页纸。在 Lean 的 Mathlib 中椭圆曲线被定义为带有 Weierstrass 方程的四元组并且带上了非奇异判别条件。Frey 曲线的构造在Mathlib.NumberTheory.Frey一类模块里实现了包括判别式和导子的计算。实际做 Fermat 定理形式化的团队光是把 Siegel 模空间、椭圆曲线的 Galois 表示、模形式的 Hecke eigenform 这些概念从论文翻译到 Lean 类型就用掉了上万行代码。2.2 从 Wiles 的论文到 Lean 代码的工程过程手工把证明写进 Lean 的工程量是天文数字这也是为什么过去三十年没有人完成——单纯靠人力敲入每个引理可能要几十年。这里 Claude 提供的价值并不是“自动给出证明”而是“把论文中的论证路径翻译成 Lean 子目标”再逐步拆解。举个具体例子。证明过程中有一个关键断言Frey 曲线的 mod 3 Galois 表示不可约并且它的 mod p Galois 表示会被诱导到某个子群上。论文里会写“通过简单计算可得”但 Lean 里你必须逐项展开表示的定义、验证模空间上的群作用、检查系数域扩张后的分解情况。这种活特别适合 AI 来干它知道目标长什么样也能生成候选步骤虽然经常失败但比人去从头翻文献快几个数量级。在实操层面你是这么用 Claude 跟 Lean 交互的Claude 生成一段 Lean 代码你在环境里跑lean编译得到错误信息后把错误喂回去Claude 再修改。这和我平时用 Claude 改 Python 代码的模式几乎一样区别在于 Lean 的错误信息更严格任何一个类型不匹配都会让它卡住。团队甚至为 Claude 设计了专门的“证明搜索”工作流先让它自动生成大量sorry占位的引理骨架再逐个把 sorry 填满最后把整个仓库编译通过作为完成标准。2.3 AI 模型在证明中的作用边界一定要澄清的是Claude 并没有做到“从零读懂费马论文然后自主想出证明”。它更像是“带工具的专家助手”——知道费马大定理的证明框架能把论文中的论证语义翻译成 Lean 表达式并对每个子目标展开战术搜索。我实测下来这种合作的模式在形式上很像结对编程人类数学家负责设定高层的分解策略指出某一步应该用哪个定理例如“这里要使用 Ribet 定理请先检查它是否在 Mathlib 里”Claude 负责处理那些机械但琐碎的 work比如把模形式的 q-expansion 展开、处理伽罗瓦作用与 Hecke 算子的交换性、证明某个映像是单射之类的局部内容。这类任务大量存在且不需要惊人创造力只要不搞错依赖关系AI 特别能扛。把 AI 当“证明实习生”这个定位很关键。如果期待它一次写出一个几十行的完整证明那大概率会失败。但如果把它当成“随时可以调用的引理证明机”每问一步只生成 3 到 10 行代码配合 Lean 的类型错误不断迭代成功率会高很多。我自己在搞 LAN 证明时单个 lemma 平均要来回 5 到 15 轮会话这和刷算法题完全不同。3. 实操指南本地复现与体验机器校验证明3.1 环境准备安装 Lean 与 Mathlib想验证费马大定理证明或者干点轻量形式化证明第一步就是把 Lean 环境装好。工具链现在用elan作为版本管理器类似 Rust 的rustup。在 macOS 或 Linux 上执行curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh装完后默认会把lean、lakeLean 的构建工具和包管理器都放到~/.elan/bin里。接着新建项目mkdir fermat-playground cd fermat-playground lake init fermat_playground math lake update这里lake init fermat_playground math的意思是初始化一个依赖 Mathlib 的 Lean 项目。Mathlib 是 Lean 数学库包含几百 MB 的定义和证明首次lake update和构建会比较久要有心理准备。如果你只想快速玩一下可以用 VS Code 安装 Lean4 插件然后打开一个只有单文件的目录也会自动弹窗提示安装环境但项目化还是推荐lake。注意在 Windows 上我建议使用 WSL 2因为 Mathlib 构建脚本对 Linux 工具链支持最好。直接装在 Windows 原生环境容易遇到git路径转义和动态库加载问题实测下来 90% 的坑都能靠换 WSL 避开。3.2 拉取费马大定理证明的项目代码费马大定理形式化证明的代码托管在 GitHub 上的ImperialCollegeLondon/FLT项目团队由 Imperial College 和微软研究院相关研究者主导Lean 社区很多数学形式化项目都挂在大学机构下。git clone https://github.com/ImperialCollegeLondon/FLT.git cd FLT lake exe cache get lake build这里的lake exe cache get很实用会从 Mathlib 的 cache 服务器拉取预编译好的.olean文件大幅跳过本地编译过程。如果你直接lake build可能要白等两个小时。拉完缓存后再 build通常几分钟到十几分钟就能编译完成具体时间取决于 CPU 核心数和内存。构建完成后你可以在项目里搜索fermat_last_theorem在src/FLT/Main.lean里看到核心定理theorem fermatLastTheorem {n : ℕ} (hn : 2 n) : ¬ (∃ a b c : ℕ, a ^ n b ^ n c ^ n ∧ a 0 ∧ b 0 ∧ c 0) : by -- 证明内容这里第一个¬就表示费马大定理断言“不存在正整数解”。一个文件里可能嵌套几十个关键定理每个前面都有详细注释建议阅读顺序从Main.lean开始然后顺着它 import 的依赖树看下去。3.3 用 Claude 辅助形式化证明的基本工作流实际用 Claude 辅助写 Lean 证明我总结了一套顺手的流程你直接照着用就行。第一步把目标定理和相关定义一起发给 Claude。注意不要只发一句话Lean 缺省上下文信息时 AI 容易胡编。正确姿势是我现在在 Lean 4 里想证明一个引理 example (a b : ℕ) (h : a ∣ b) : a ∣ b * b : by然后把 Mathlib 里相关的simp、linarith、omega策略告诉它让它先尝试用最简单策略解决。第二步拿到 AI 生成的代码后不要直接全量编译。先只复制目标 lemma 到本地文件用lean单独编译。如果报错把错误信息原样贴回给 Claude。这里有个小技巧Lean 的错误信息经常很长我通常会保留前 20 行和最后 15 行中间的错误栈其实对 AI 判断影响不大反而太长会稀释关注点。第三步面对长时间无法解决的 lemma换成“先加 sorry 占位补依赖”的思路。比如证明一个超大定理前先写上by sorry让它通过然后逐个定理把 sorry 消除。这种“自上而下占位自下而上填充”的顺序是大型形式化项目能否进行下去的关键。我拿一个真实例子說明。有一次我想证明“两个数互质且其中一个整除乘积则该数整除另一个”。先发给 Claude它给了我example {a b c : ℕ} (h : a.coprime b) (h1 : a ∣ b * c) : a ∣ c : by exact h.coprime_dvd_of_dvd_mul_left h1结果编译不过报错说coprime_dvd_of_dvd_mul_left这个定理不存在或签名不匹配。我搜了下 Mathlib 文档发现正确名字是Nat.Coprime.dvd_of_dvd_mul_left。把错误反馈给 Claude 后第二次生成就通过了。这样来回几轮你对 Mathlib 的 API 也会越来越熟。3.4 一个可以复现的最小实例证明根号 2 的无理性Fermat 大定理的完整证明门槛太高但你可以从一个小一点的经典证明体验“机器校验”的乐趣。比如证明√2是无理数。在 Lean 里大致写法是import Mathlib.Data.Real.Irrational theorem sqrt_two_irrational : Irrational (Real.sqrt 2) : by have hsqrt : (Real.sqrt 2) ^ 2 2 : by rw [Real.sq_sqrt] norm_num -- 这里借助 Mathlib 已有的 irrational_sqrt_two_iff 来证明 exact irrational_sqrt_two实际上 Mathlib 早就内置这一结论你直接exact irrational_sqrt_two就能过。你真正该做的实验是把这行定理替换成自己的版本比如证明√3的无理性方法类似import Mathlib.Data.Real.Irrational import Mathlib.Analysis.SpecialFunctions.Pow.Real example : Irrational (Real.sqrt 3) : by exact (irrational_sqrt_iff.mpr (by norm_num : ¬ ∃ n : ℕ, n * n 3))这行代码能让你感受到形式化证明的“粒度”它不像数学书里写“若能写成最简分数 p/q 则矛盾”而是直接把“不存在整数的平方等于 3”转换为机器可检查的命题再把证明拆解给现有定理。如果你能把这行编译通过你对 Lean 的类型、证明策略、Mathlib 的用法就有直观认识了。4. 踩坑记录与常见问题排查实录4.1 Mathlib 编译慢、内存爆掉怎么处理很多新手第一次lake build时发现内存占用飙到 10 GB 以上直接卡死。这不是你系统问题是 Mathlib 本身就大。解决办法是不要全量编译尽量只构建目标依赖lake build FLT把目标限定到你所在的包名Lean 构建系统就不会把所有文件都编一遍。另外 Lean 进程默认不会做太多 GC 调优如果你内存吃紧可以在lakefile.toml里设置更保守的 worker 数或者用lake build -j 2限制并行任务减少同时编译的文件数量。4.2 依赖版本不一致一编译全是红Lean 生态更新很快Mathlib 还在频繁改动定理名字。一个月前写的代码一个月后可能就编译不过了。遇到这种问题最稳的方法是让项目和 Mathlib 版本保持锁定在lakefile.toml里看require mathlib的指定 commit 或 tag。[[require]] name mathlib git https://github.com/leanprover-community/mathlib4.git rev v4.15.0如果你只想跑费马大定理那个仓库克隆后千万不要擅自lake update mathlib否则很可能把项目锁定版本弄乱然后冒出几百个错误。就老老实实用它默认的缓存和依赖版本。4.3 AI 生成的证明存在“证伪”和“幻觉”问题用 Claude 写 Lean 证明时最大的坑是你没法一眼看出它生成的代码对不对。有时它看起来很长、结构很严谨但编译时暴露出一堆未定义变量和类型错误。更危险的是它偶尔会“换一种形式”输出一个看似等价的断言但实际改变了命题强度然后靠 sorry 或者axiom糊弄过去。我在查 AI 生成代码时有一条铁律禁止任何axiom、sorry、admit出现在最终的编译通过版本中。在大型项目中可以用guard_target和set_option pp.all true输出展开后的目标帮你看清楚它到底在证什么。如果某个证明片段用了 50 行以上我会拆成多个小 lemma让每一段都能单独编译这样可以精确锁定错误位置。4.4 形式化证明和测试的区别这一条写给搞软件工程的读者。很多人问“AI 写 Lean 证明这么多限制为啥不干脆写几千个测试用例来验证费马大定理”这是本质区别测试只能证明“我试过的这些输入没问题”形式化证明证明“所有可能的输入都没问题”。比如费马大定理你即使跑了天文数字次 a、b、c也不能排除下一个反例但 Lean 证明一旦通过在逻辑上就没有反例存在的空间。换个更工程化的例子当你写一个支付系统测试保证“这 100 条用例没出错”而验证保证“所有满足前置条件的交易余额都不会为负”。后者很难但一旦做到整个系统的核心逻辑就绝对可信。现在 Claude 让这个“很难”变成可能因为它给形式化验证降低了上手门槛。这也解释了为什么形式化证明这一波被很多人视为软件工程的下一场革命。5. 这件事对程序员、数学家与 AI 研发者的真实影响5.1 对软件开发者从“测试驱动”走向“证明驱动”模式匹配一下就能发现Lean 里写证明的函数式思路和日常写 Rust、Haskell 很像。形式化证明并不只是数学家的玩具它在智能合约、编译优化、安全关键逻辑验证上都有直接价值。比如你写了一个分布式共识算法传统做法是写一堆仿真测试未来你完全可以把共识协议写成 Lean 里的定理让机器证明它在任意消息序列下都能满足 safety。Claude 这类模型对形式化验证的加速作用很明显。过去写一个协议验证需要极强的类型论功底现在只要会说“帮我证明这个不变量”就能起步。我自己就用 Claude 成功验证过一个小型状态机的不动点性质整个过程大约 3 小时如果纯手工查文档可能得 3 天。这种“门槛高但 AI 能垫脚”的领域接下来会有大量新工具出现。5.2 对 AI 安全与智能体研发形式化证明防止不可控行为最近业界流行“智能体安全”的说法核心矛盾是让模型自由操作外部环境时保证它不做危险的事。费马大定理的形式化证明给了一条新思路与其让模型“保证不犯错”不如针对关键模块建立可证明的不变量再用 Lean 等系统去验证。这和 Claude 做数学证明是同构的——模型负责提出行动策略和证明候选验证器负责裁决正确性。没有形式化验证AI 生成的逻辑再流畅也可能是幻觉有了它至少最后的决策边界是可审计、可证明的。这也意味着“智能体不是不能犯错而是犯的错能被限定在可接受空间里”。比如在自动改代码的流程里你可以用 Lean 验证循环不变量保证 AI 补丁不会破坏某些核心属性。目前这还只是研究前沿但方向已经清晰。5.3 对普通开发者的机会在哪里看到这里你可能会想费马大定理和我有什么关系我觉得机会在三个层面。第一把形式化验证应用于业务代码的关键模块。比如说金融计算里的浮点误差、排序算法的不变量、缓存一致性协议都能从“测试覆盖”升级到“证明覆盖”。第二吃透 AI 辅助证明的工作流这在以后会是编程领域的“高阶技能”类似二十年前会写单元测试。第三直接参与到 Mathlib 这样的开源数学库建设里把日常工作之外的证明贡献进去既能提升自己逻辑能力也是在积累开源信用。不要被“数学博士”三个字吓退。我在实际使用中发现Lean 的证明语言很大程度是枚举式、搜索式的不是纯粹智力比拼。你只需要具备基本的数理逻辑功底加上会用 Claude 搜索策略就能开始写一些有价值的实际证明。比起读十年数学博士这门槛已经低太多了。6. 写在最后的一点个人体会费马大定理的全机器校验形式化证明公布后我连夜把项目拉下来编译了一版。看着终端里跳出No errors的时候我心里其实挺不是滋味的三百多年的人类最高智慧结晶就这么被拆成了几十万行机器可读的逻辑代码——不是被贬低而是被彻底锁定。Claude 在这个过程里不是主角但它是那根让整个工程变成“几个月而不是几十年”的杠杆。如果你也想动手我的建议是从小目标开始比如一个∃ n, 2 ^ n n ^ 2的证明或者你自己代码里一个关键的幂等性断言把它让 Claude 写成 Lean再亲自跑通。踩几个坑之后你会获得一种和普通编程完全不同的确定感当你真的编译通过一个复杂证明时你会意识到这台机器对一个数学真理的信任程度已经超过了绝大多数人的“我觉得没问题”。