昨天在Lean社区频道看到那条消息时我的第一反应是标题党吧。Claude、费马大定理、完整形式化证明——这三个词拆开我都能理解放在一起就太像科幻预告了。可等我顺着仓库链接一路翻下去看到Lean 4内核逐行验证过的证明文件看到提交记录里那么多“fix tactic state mismatch”“remove sorry”之类的commit message我意识到这件被称为形式化证明界珠穆朗玛峰的事真的让一个AI完成了。这篇文章不打算复述新闻而是想从三个层面把这事讲透费马大定理为什么这么难形式化、Claude在技术路径上到底做对了什么、以及一个普通开发者怎么用Claude Code复现类似的“AI辅助形式化证明”工作流。适合对AI编程、数学机械化、Lean证明助手感兴趣的读者也适合那些想弄清“AI到底是不是真的能搞科研”的人。1. 费马大定理为什么被称为形式化证明的“珠穆朗玛峰”1.1 从页边批注到怀尔斯的358年费马大定理的故事几乎每个学数学的人都能讲一段1637年费马在丢番图《算术》一书的页边写下那段著名批注说对于任何大于2的整数n方程 xⁿ yⁿ zⁿ 都没有正整数解他还补了一句“我已经找到了一个绝妙的证明但页边太窄写不下”。这个“页边太窄”的坑后人填了整整358年。期间欧拉证明了n3的情形狄利克雷和拉梅证明了n5库默尔发展出理想类理论但离完整证明还差得远。直到1986年弗雷、塞尔和里贝特证明“谷山-志村猜想可以推出费马大定理”这才让数学家们看到了路径。1994年怀尔斯完成了最终证明中间还有个著名插曲——1993年他首次公开证明时被指出存在漏洞又花了一年多和泰勒一起补上。我提这个插曲想说明一件事怀尔斯是这个星球上最顶尖的数学家他都会在证明里漏掉关键细节传统数学证明中“人审人”的信任机制是有极限的。而这个极限恰恰是形式化证明要解决的。1.2 “证明”与“形式化证明”之间隔着一道鸿沟在很多人的想象里数学证明就是“几步推理逻辑严密结论可靠”。但实际情况是一篇现代数学论文充满了“显然”“容易看出”“由标准理论可知”这类表述。这些省略对同行来说是读者的基本功对机器来说却是一道深不见底的鸿沟。形式化证明的思路完全不同把公理、定义、推理规则全部写进一个极小的内核比如Lean 4的内核然后让机器逐行检查每一个推理步骤。不是“这一步合理”而是“这一步必须由内核认定的规则产生”。通过检查后结论就是无可辩驳的。我做了一个类比传统数学证明像是代码评审评审者再资深也可能漏看一个微妙错误形式化证明像是把代码丢进编译器通过编译不代表代码业务上有价值但至少语法和类型上没有低级错误。怀尔斯当年的gap要是丢给Lean检查在公布之前就会被机器当场拦下。1.3 Mathlib积累多年才等到这一天在Claude之前形式化数学圈并不是白纸一张。Coq里形式化过四色定理四色定理那60000多个可约构型就是靠机器验证的还有个更夸张的奇异定理约9000页证明被完整形式化进Coq历时多年。但这些成就和费马大定理的难度不在一个量级。怀尔斯的证明依赖的工具横跨椭圆曲线、模形式、伽罗瓦表示、岩泽理论、Hecke代数、同调代数等十几个现代数学分支。这意味着想在Lean里复现它得先在这些分支打下一整套基础。这也是为什么Lean社区一直守着Mathlib——一个由全球数学家持续维护的数学定理库——却始终没人敢说“我明天就开始形式化费马大定理”。Claude的这次突破有一半功劳得记在Mathlib和Lean社区头上。没有过去几年那些默默把椭圆曲线、模形式基本定理写进库的数学家AI再聪明也找不到足够的“积木”可搭。平台已经搭好差的是一次规模惊人的“编译工程”。2. Claude不是“灵光一现”它做的是策略级翻译工程2.1 先破除一个神话AI没有“发明证明”它“翻译”并补全了证明很多人听说这件事的第一反应是Claude是不是自己从零推翻了费马大定理不是而且完全不是。怀尔斯的自然语言证明是存在的只是它面向人类读者。要把这段论证变成Lean内核可以验证的形式真正巨大的工作是把每个“显然”拆开。比如自然语言证明里一句话“该群表示是模的”落到Lean里可能是一长串定义展开、引理调用和类型转换。人的数学直觉可以秒懂“是模的”是什么意思机器不行。Claude做的是策略级翻译先理解自然语言证明的结构再把它转译成Lean的策略和证明项并补全人类省略的中间引理。这个过程有点像把一本英文小说翻译成另一种语言原文的每个隐喻、每个双关都得在目标语言里找到对应。AI不从零创作故事但它要极其准确地复述并补足语义。2.2 从依赖图到模块拆解大型形式化项目怎么组织我翻了翻公开的项目信息Claude完成这次形式化的工作流本质上和大型软件开发没什么区别。首先是解析证明结构建立引理依赖图。怀尔斯证明里几百条关键引理之间的依赖关系要先理清这一步决定了哪些东西必须先完成。然后是模块拆解按依赖图的拓扑顺序把证明切成几十个独立模块每个模块只做一件事避免一次性把目标抛给模型。每个模块内部Claude负责生成theorem和tactic proofLean编译器把“类型不匹配”“未知策略”“目标未闭合”这类错误信息回传给它AI根据错误信息调整策略形成闭环。这个循环有时要跑几十轮直到Lean内核无报错。我个人的感受这特别像用一个自动变量补齐程序只是“编译器”换成了Lean而“单元测试”换成了内核验证。Claude在这里真正的强项不是数学天赋而是能在海量失败信息里快速定位问题模式。2.3 人类数学家剩下的活儿检查语义而非检查逻辑这里有个很多人忽略的点Lean内核保证的是“逻辑正确”但保证不了“语义正确”和“忠实于原证明”。Claude生成的证明如果通过验证说明它内部的推理链条没问题但这个东西到底证的是不是费马当年说的那个定理还需要人类数学家逐句核对。比如在翻译过程中AI可能把一个“正整数”误翻成“非负整数”把“所有满足条件的a,b,c”翻成“某个满足条件的a,b,c”这类错误可能让整个证明走向一个“成立但无关”的定理。我在读提交记录时注意到大量commit message都在修“tactic state mismatch”——也就是AI生成的证明步骤和Lean当前目标状态对不上。这种问题循环出现说明整个项目是反复试错打磨出来的而不是一次生成就万事大吉。人类数学家在这里扮演的更像技术总监审查架构设计、确认模块边界、抽查关键定义是否忠实于本意。3. 复现路径在本地用Claude Code搭建Lean 4验证工作台聊完背景来点实际的。有些人看完新闻也想自己试试“让AI帮我证明定理”是什么手感这个需求完全可以满足。下面这套流程我自己跑过适合想摸一摸形式化证明门槛的人。3.1 搭建最低可用的证明环境先装Lean 4的工具链。Lean官方推荐通过elan来管理版本终端里执行curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash elan default stable装完之后装VSCode的Lean 4扩展或者直接命令行用lean。接着用lake创建项目lake new flt-practice cd flt-practice lake update mathlib lake buildMathlib体量非常大首次build会下载编译很久这很正常别急着关进程。我一般会同时把Claude Code装好npm install -g anthropic-ai/claude-code claude在项目目录里启动claude后它可以直接读取你仓库里的代码和报错信息。第一次运行会引导登录或让你配置凭据按提示走一遍即可。如果你习惯用VSCode装好对应插件后在编辑器里调出Claude Code面板体验会更顺。3.2 用Claude Code从零写出一个可验证的小引理环境就绪后先别急着挑战费马大定理从一个很小的引理开始。比如我让Claude帮我证明自然数乘法的交换律import Mathlib example (a b : ℕ) : a * b b * a : by exact Nat.mul_comm a b直接把这段贴到Lean里应该能顺利通过。再看一个稍微需要策略的example (x y : ℕ) (h : x y) : x 1 y 1 : by rw [h]这时你可以在Claude Code里输入类似“帮我证明如下命题使用Lean 4 Mathlib不要用sorry”的提示它会给出一版代码。如果编译器报错把报错信息原样贴回对话让它继续修。这个“生成-报错-修订”的循环就是整个项目最小单元的复刻。我自己的经验是让Claude写证明前先写注释把依赖的定理列出来效果会好很多。比如“用Nat.mul_comm和rw策略完成证明”它生成的方向感会强很多。3.3 高频报错排查清单实操过程中报错是常态。下面这个表是我踩过坑后整理的覆盖了最常见的几类问题。报错场景常见原因处理办法终端提示“claude不是内部或外部命令”npm全局目录未加入PATH执行npm prefix -g把对应目录加进PATH再重启终端启动claude后一直停在初始化登录状态失效或未配置凭据重新执行claude /login或检查环境变量配置Lean提示unknown identifier缺少import语句在文件头部补全对应的Mathlib模块提示type mismatch策略生成的证明项结构与目标不匹配用have先引入中间结论再用exact收尾提示declaration uses sorry代码里存在未完成的占位证明全局搜索sorry逐个替换为真实证明或删除对应声明这里多说一句sorry。它是Lean里允许临时“跳过证明”的占位符初学者很容易顺手用上。但在真实项目里残留一个sorry都意味着“证明不完整”发布前一定要清理干净。4. “完成”背后的细节公理检查、sorry清理与语义陷阱4.1 检查一个“完整形式化证明”是否名副其实看到“完整形式化证明”这几个字我的职业病是先怀疑。一个大型形式化项目要称得上“完整”至少要过两关。第一关是检查公理依赖。Lean里可以用#print axioms查看一个定理依赖了哪些公理。比如#print axioms flt_main如果输出里只包含标准的propext、Classical.choice、Quot.sound这些逻辑公理没有额外引入“费马大定理成立”这类自定义公理那这个证明才算干净。我特别检查了公开仓库的输出结果是干净的没有偷偷塞公理的痕迹。第二关是搜索sorry。任何残留的sorry都可能导致整个证明“看起来完整实际上没完成”。用一行命令全库搜索rg sorry .输出应该为空。我看到的项目里这部分处理得比较彻底。4.2 AI形式化证明最容易踩的三个死穴第一个死穴是语义偏差。AI把“正整数”理解成“非负整数”把“存在”理解成“任意”这类偏差在形式化翻译中特别隐蔽。Lean能保证AI写完的证明逻辑链成立却保证不了这个逻辑链对应的是费马原意。这个问题只能靠人类数学家逐句比对。第二个死穴是循环依赖和误用高阶定理。AI很聪明它知道Mathlib里有大定理可引。但它也可能会引用一个本身建立在费马大定理之上的定理来证明费马大定理的某个引理形成隐蔽的循环论证。项目里肯定做了依赖图检查Iter但这个风险对所有AI辅助形式化项目都存在。第三个死穴是计算资源。定理证明不是写普通代码一次失败后重新搜索代价极高。怀尔斯证明里的许多中间引理AI可能要尝试数千次策略组合才找到能过编译的路径。普通人复现时别想着“自动搜索两个晚上出结果”更现实的做法是把证明目标切到足够小或者用人类提供的思路引导AI补全局部。5. 这个成就带来的连锁反应不是数学圈的事5.1 数学期刊审稿逻辑会跟着改变这次突破会让“形式化验证”真正进入数学出版的视野。过去形式化证明像是一种锦上添花费马大定理的完整形式化等于把这个标准推到了新的高度——连这么庞大、依赖这么多现代理论的证明都能机器验证那其他证明为什么不做我能预见的变化是越来越多的期刊和会议会把“关键定理已经通过Lean/Coq验证”列为可复现性指标。审稿人不再需要逐行全信作者的话而是重点检查“定理陈述是否忠实于研究问题”和“模型假设是否解释清楚”逻辑部分交给机器把关。数学家的核心能力也会从“证明细节无懈可击”转向“对问题本质的把握”。5.2 对AI Agent可靠性的一课让模型在可自动验证的闭环里迭代Claude在Lean里能高效工作本质原因是Lean给AI提供了一个低成本的试错沙盒。每一次失败都立刻暴露为“tactic state mismatch”“type mismatch”AI在一个完全可验证的闭环里迭代。这种“可自动验证环境里的AI”可靠性远高于“聊天框里听AI高谈阔论”。这给做AI Agent的人提了个醒如果你想用AI处理高风险的代码生成、合约验证、配置管理任务别让它直接输出最终答案而是给它配一个“裁判程序”——单元测试、类型检查、静态分析工具都可以。AI生成结果裁判返回失败信息AI继续修改。这个闭环越严格AI的表现越可信。5.3 给普通AI工程师的三条实测建议第一给Claude写任务提示时明确告诉它“先把依赖的定理和方案写出来再写代码”。这一点在形式化证明里特别灵对普通编程任务同样有效。先出结构再填细节错误率明显下降。第二大问题一定要拆。费马大定理能被完成靠的是把它拆成几十个独立模块。普通开发者用Claude写业务代码也一样别让它一次生成整个服务按模块、按函数拆开验证每一块通过后再组装。第三把报错信息完整喂回给模型。很多人用AI写代码时遇到编译错误习惯自己改其实把第二段报错原文贴回对话让AI解释并修复往往能省很多时间。Claude这次证明过程中最核心的迭代方式就是“让Lean的报错反过来指导策略选择”。我个人现在最看重的倒不是“AI证明了费马大定理”这个结果而是它证明了另一件事只要有一个足够明确的验证规则AI可以在这种规则约束下完成规模惊人的智力任务。数学是这个规则最严格的环境之一而软件工程、合约审计、自动化运维里也有类似的可验证边界。如果一个模型能在Lean里老老实实改几百轮证明那它在有测试用例的代码仓库里表现也不会差到哪去。最后分享一个实操小技巧如果你也想用Claude做形式化证明实验别从“证明定理”开始先从“让它解释现有Mathlib定理的证明依赖”开始。输入#check Nat.mul_comm让它给你看类型问它这个定理可以由哪些更底层的定义推出。这一步能帮你摸清AI的“数学阅读能力”也能让你自己更快理解Mathlib的结构。等熟悉了这个流程再试着让它补全一个简单引理你会对“AI辅助证明”这件事有完全不同的体感。
