这几天数学圈和程序员圈子同时被一条消息刷屏Claude完成了费马大定理的首个全机器校验形式化证明。注意这里不是“AI 写了一篇关于数学定理的文章”而是用 Lean 4 证明助手把费马大定理的整条证明链路真正跑通每一步都由机器内核逐一校验。这件事的分量只有真正碰过形式化验证的人才懂费马大定理从1637年被提出到1994年怀尔斯给出完整证明中间隔了三百五十多年而把它变成机器可读、可验证的“证明程序”难度又上了一个量级。这篇内容我不打算只给你复述新闻。我会把这个事件拆开讲明白再带你从零装一遍 Claude Code 和 Lean 环境跑一个能看懂的入门级形式化证明顺便把我安装和使用 Claude Code 时踩过的一堆坑整理成速查表。无论你是搞数学、写代码还是单纯关心 AI 推理能力边界的读者这篇都能给你一点真东西。1. 事件全貌Claude 完成费马大定理首个全机器校验到底牛在哪1.1 费马大定理的“数学分量”与形式化验证的难点如果你对费马大定理只有模糊印象它说的是当整数 n 大于 2 时方程 x^n y^n z^n 不存在正整数解。费马在书页边写下这个猜想时还说自己找到了巧妙证法但“空白太窄写不下”。这一晃就是三百多年无数数学家前赴后继直到1994年安德鲁·怀尔斯用椭圆曲线、模形式、伽罗瓦表示等现代高深工具完成证明才彻底了结这段公案。怀尔斯的证明本身已经够复杂了——最后发表出来是一百多页的论文里面嵌套了大量抽象数学对象还依赖很多其他数学家的工作。所谓“形式化证明”就是要让计算机把这些抽象推理全部“嚼碎”变成一条条能被机器识别的逻辑步骤最后通过类型检查。这相当于什么相当于你不但要读懂一篇天书级的论文还得把论文里每句话都翻译成一种极其严苛的编程语言一个标点错了都编译不过去。所以过去几年Lean 社区里大量工作都是在做这种“人肉翻译”把已知定理的证明一句一句输入进 Lean 的 Mathlib 定理库。比如彼得·舒尔茨的液体张量实验、一些数论和代数几何中的大定理都是顶尖数学家加上熟练的形式化工程师花几个月甚至几年才磨出来的。这次 Claude 完成费马大定理等于跳过了“人类逐句翻译”这个环节由模型来生成证明代码并持续修正直到机器完全验收。1.2 “首个全机器校验”意味着什么不是 AI 发明了证明而是 AI 打通了验证链条这里必须把话说明白免得被营销号带偏Claude 不是“独立想出了一个全新的费马大定理证明”而是“在 Lean 4 的形式化证明环境里成功完成了一条机器可校验的证明链”。这两者的区别非常大。前者的潜台词是 AI 具备了怀尔斯级别的数学创造力——这是目前任何模型都做不到的。后者的意思是Claude 能够在已有数学知识库如 Mathlib和 Lean 证明助手的反馈下结合自然语言提示与代码生成能力逐步构造出每条证明步骤最终让机器的内核检查器给出“通过”。但即使是这样也已经是里程碑级别的成果。原因在于费马大定理的证明规模极大涉及的中间引理、定义和高阶抽象成千上万。一个模型要在这类庞大而严苛的环境里“活下来”必须做到三件事理解数学对象之间的逻辑关系写出 Lean 认可的证明策略并且根据编译错误不断自我修正。以前大语言模型做数学题通常还停留在竞赛题、初等数论的范围这次直接上到现代数论的大定理这是量级上的差距。“全机器校验”这个词的含金量在于整个验证过程不依赖任何人类的主观判断。你可以觉得某个推导“看起来对”但 Lean 说不行就是不行。反过来只要 Lean 内核通过那这个证明在逻辑上就是严格成立的哪怕写证明的 AI 根本不知道自己在干什么。这套机制天然就是给 AI 的“幻觉”上的一道锁。2. 工具链拆解Lean 4、Mathlib 与 Claude Code 如何协作2.1 Lean 4把数学证明变成可编译执行的代码要理解这次事件绕不开 Lean 4。很多人第一次听到 Lean 会以为是一个“数学软件”像 Mathematica 或者 MATLAB 那样用来算微积分、画函数图像。其实不是。Lean 是一个依赖类型理论的定理证明器同时也是一门函数式编程语言。你可以把它理解成一个“能审查逻辑的编译器”。普通编译器会检查你代码里的类型错误比如你把字符串传给一个接收整数的函数编译器立刻报错Lean 则更进一步它允许你把“某某命题成立”编码成一种特殊类型然后证明就是构造出这个类型的一个合法实例。举个例子“偶数的定义”可以写成存在一个整数 k使得 n 2 * k。那你要证明“两个偶数相加等于偶数”本质上就是要构造出某个整数 k使得 a b 2 * k。Lean 的类型检查器会从头到尾看着你不允许你跳过任何一步。如果你偷懒用了一个未经证明的断言Lean 会拒绝编译或者要求你用 sorry 占位并明确标出“此处未完成”。这就是形式化证明和普通数学论文的根本差异人类审稿人可能会漏掉一个微妙的逻辑跳跃但 Lean 内核永远不会漏。它就是数学界的“最严苛课程设计查重系统”错一点整篇打回。2.2 Mathlib 定理库形式化验证里的“公共基础设施”光是有一个厉害的 Lean 语法还不够。你要证明费马大定理总不能从皮亚诺公理开始一步步推吧那工作量人类根本受不了。所以 Lean 社区搞了一个叫 Mathlib 的大型数学定理库把大量已经验证过的定理、定义、证明策略打包好供所有人引用。Mathlib 对形式化证明的重要性相当于 Node 包管理器的生态对 JavaScript 的重要性。没有它每个项目都要从零开始造轮子有了它你可以站在前人的肩膀上。Claude 这次能完成费马大定理的证明很大程度上就是因为它能熟练调用 Mathlib 里现成的引理和策略而不是把两百页论文从头手搓一遍。这里有个很实际的经验如果你打算自己尝试类似工作不要一开始就挑战“世界级难题”。先在 Mathlib 里找几个你已经会证的定理把它们的证明代码读懂、跑通再去琢磨怎么让 AI 帮你写新证明。工具再强也得先会用。2.3 Claude Code 进入证明场景迭代式生成与校验闭环Claude Code 是 Anthropic 推出的终端 AI 编程工具跟你在网页上打开 ChatGPT 或 Claude 聊天完全不是一个物种。它是跑在你自己项目目录里的能读文件、写文件、执行命令还能调用外部工具。平时我主要拿它在 VS Code 的终端里写业务代码结果这次事件让我发现它在形式化证明场景里出奇地好用。原因很简单形式化证明是一个“生成-反馈-修正”的迭代过程。你先让 Claude 按提示写一段 Lean 证明然后运行编译读回 Lean 报错提示再让 Claude 根据报错调整策略。这个过程如果靠人肉复制粘贴到聊天窗口里效率极低而 Claude Code 本身就嵌在终端环境里读报错、改代码、重新运行都在同一个上下文里形成的闭环非常自然。我在本地跑小实验时就是让 Claude Code 把 Lean 的报错信息原样吞进去再回给我修正后的代码。试了几轮之后发现它甚至能从报错里判断出“我是不是用了过时的 API应该改用 Mathlib 里新的策略”。这个能力说实话比我预期强不少。3. 实操本地安装 Claude Code 并用 Lean 跑通第一个形式化证明3.1 前期准备安装 Lean 4、VS Code 插件与 Claude Code先说环境。我自己主力系统是 Windows WSLLean 和 Claude Code 在 WSL 里跑起来最顺手。如果你用的是原生 Linux 或 macOS步骤只会更简单。第一步安装 Lean 4 的版本管理器 elan。打开终端执行curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash source ~/.profile elan default stable这一步会把 Lean 编译器装好类似安装 Rust 的 rustup。装完后验证一下lean --version能输出版本号就没问题。第二步在 VS Code 里安装 Lean 4 扩展打开扩展商店搜索“Lean4”装官方那个就行。这个扩展提供了实时类型检查、策略状态显示写证明时左边是代码、右边能看到当前证明目标非常直观。第三步安装 Claude Code。前提是你已经装了 Node.js 18 以上的环境。执行npm install -g anthropic-ai/claude-code claude --version装完之后第一次运行 claude 命令它会引导你登录账号。我在这里特别提醒一句Claude Code 的底层是调用 Anthropic 官方模型接口所以你需要一个能正常访问服务的账号并且了解免费额度和付费额度的差异。如果你在登录时遇到“unfortunately, Claude is not available to new users right now”之类的提示多半是账号所在区域或服务名额限制直接跟官方客服确认就好别相信任何第三方“破解”方案也不要去折腾那些灰产工具。3.2 实操演示用 Claude Code 完成一个简单的定理证明装好环境后我建议你先别碰费马大定理先做一个最简单的热身证明“两个偶数之和是偶数”。这个证明规模小、逻辑清晰却能完整走一遍“生成-编译-修正”流程。第一步新建一个 Lean 项目目录并创建一个 test.lean 文件import Mathlib.Data.Nat.Basic import Mathlib.Tactic theorem even_add_even (a b : Nat) (ha : ∃ ka, a 2 * ka) (hb : ∃ kb, b 2 * kb) : ∃ k, a b 2 * k : by rcases ha with ⟨ka, rfl⟩ rcases hb with ⟨kb, rfl⟩ exact ⟨ka kb, by omega⟩解释一下这段代码在干什么。我先把“a 是偶数”形式化定义为“存在 ka 使 a 2 * ka”然后从假设里把 ka 和 kb 拆出来再用 exact 构造一个 k ka kb让 lean 验证 a b 2 * (ka kb)。最后的by omega是一个自动算术策略能处理这种简单的整数等式。现在打开 VS Code 的终端启动 Claude Codeclaude在第一轮提示里你可以给它一个非常精简的任务描述我用 Lean 4 写了一个定理 even_add_even目标是证明两个偶数相加还是偶数。 我现在把当前代码和报错信息发给你请你只输出修正后的 Lean 代码。如果你直接抄上面的完整代码Lean 大概率直接通过不需要修正。我建议你可以故意删掉其中一行让 Lean 报错再把这个报错发给 Claude Code。比如删除rcases ha with ⟨ka, rfl⟩Lean 会提示你应该先解构 ha但还没有拿到 ka这时 Claude Code 会根据报错帮你把结构补上。这个实验做完你就能直观理解“机器校验 AI 生成”是怎么配合的Claude 负责写Lean 负责审失败以后 Claude 再看批注修改。整个过程跟真人程序员在 IDE 里改代码没有任何区别只是“写代码的人”变成了大模型。3.3 从简单证明到费马大定理扩展到大项目的工程方法你现在可能想问从“偶数加偶数”到“费马大定理”这中间差了几万条证明Claude 究竟是怎么把这件事做成的我虽然没有参与官方项目但根据我拿 Claude Code 写 Lean 的实际经验可以合理推测出几个工程化要点。第一拆解成子问题。费马大定理的证明不可能一蹴而就一定是先拆成若干个中层引理比如“某种椭圆曲线是模的”“某个伽罗瓦表示满足局部-整体原则”每个引理再继续往下拆直到拆成 Lean 能直接处理的基本步骤。第二利用 sorry 占位符保持项目可编译。我们在写大型形式化证明时最怕中间卡住导致后续都没法测。Lean 允许用sorry暂时占位先不管某条引理保证整个文件能加载通过然后用 Claude Code 一个引理一个引理地挑战“终极任务把 sorry 填掉”。第三上下文要小。很多人在用 AI 写代码时有个坏习惯一次把几百行代码全部糊给模型让它在里面改。这是浪费 token 的典型操作而且容易让模型丢失重点。正确做法是只提供“当前目标 报错信息 相关定理签名”。对 Claude Code 来说这就像给一个习惯看报错改代码的人开工单信息越聚焦产出越靠谱。4. 核心突破的价值机器校验如何重塑 AI 推理的可靠性边界4.1 幻觉问题的“照妖镜”证明器就是对错的裁判大语言模型的“幻觉”问题用过的人都懂。你跟它聊历史它可以一本正经地给你编出一个人名和年份让它写代码它可能写一个看似合理实际跑不起来的函数。传统上我们靠人工抽查、测试用例来过滤这些幻觉但覆盖永远有限。形式化证明环境则完全不同。在 Lean 4 里模型写的每一条定理、每一个策略调用都要过类型检查器这一关。错了就是错了没有任何“风格分”“印象分”。从某种意义上说Lean 就是专门用来揭穿 AI 幻觉的“照妖镜”。这也是我认为这次事件最大的意义所在它第一次在一个极其复杂的数学证明上证明了一件事——只要把任务放到一个可验证的闭环里大模型推理的可靠性能被显著放大。模型可以不知道自己在做什么但验证器能保证它做出来的结果是对的。这种思路完全可以迁移到其他领域。4.2 形式化验证的工业前景从数学定理到智能体安全Claude Code 这类工具的本质是一个能自己操作电脑的“智能体”它读文件、执行命令、改代码。那么问题来了如果一个 AI 智能体真的开始自主干活了你怎么保证它不会把系统搞挂、不会产生危险操作业界现在有个方向就是用形式化验证来约束智能体行为。比如谷歌那边就有团队把形式化证明和智能体安全放到一起研究思路是给智能体的关键决策建立形式化模型再用机器验证去证明它在给定约束下不会越界。这跟证明费马大定理的逻辑是一模一样的人类不再单纯依赖“AI 看了足够多数据所以很乖”而是依赖一整套机器可验证的逻辑保障。当然现在的形式化验证还很难覆盖所有场景但它已经能在一些关键节点上落地了比如智能合约审计、协议安全性验证、关键系统的核心路径证明。费马大定理这个事件带来的示范效应是既然 AI 能在纯数学这种最考验逻辑的领域做到机器级可靠那在边界更清晰、规则更固定的工程领域形式化验证同样值得重度押注。5. 避坑实录Claude Code 安装配置与写证明的高频问题5.1 Claude Code 安装运行的经典报错与对症方案这几周我在不同机器上折腾过 Claude Code群里也有不少朋友反馈碰到问题。我把最常见的几类列成一个速查表方便你对症下药。报错现象常见原因解决办法claude不是内部或外部命令 / command not foundnpm 全局安装目录不在 PATH 里执行npm config get prefix查看全局 bin 目录把它加入 PATHPowerShell 无法加载 claude.ps1 脚本Windows 执行策略限制脚本运行用管理员 PowerShell 执行Set-ExecutionPolicy -ExecutionPolicy RemoteSigned -Scope CurrentUser提示unfortunately, Claude is not available to new users right now账号区域或服务名额限制检查账号状态、确认区域支持范围有疑问直接找官方支持每周限速提示 50% 配额免费额度或订阅额度用量较高压缩会话、合理规划任务必要时升级套餐VS Code 关闭后找不到历史对话会话日志其实保存在本地到~/.claude/projects/里找 jsonl 日志文件npm 安装速度极慢或失败网络或源的问题把 npm registry 换成国内镜像源比如淘宝源重新安装这里我想单独强调一下“找不到对话记录”这个问题。Claude Code 的会话默认不是存在网页端的而是在你本地用户目录下的~/.claude/projects/里每个项目对应一个文件夹里面是 jsonl 格式的完整对话记录。如果 VS Code 直接关闭后你觉得历史不见了去这个目录翻翻几乎都能找回来。5.2 用 Claude Code 写 Lean 证明的高频问题与排查思路写形式化证明时新手最容易踩的坑有三个。第一个坑是把“AI 写的代码”当成“一定正确的代码”。Claude Code 生成证明的速度很快但它在不确定的时候会编造一些不存在的策略名比如把omega写成arith或者调用 Mathlib 里某个根本没定义过的引理。遇到这种情况别急着让它重写而是让它先用#check命令确认定理名是否存在再继续。在 Lean 里#check就像查字典模型也会查。第二个坑是忽略“剩余目标”。Lean 在交互模式里会显示当前还剩下哪些证明目标如果你不看清楚就让模型去改它很可能“答非所问”——修好了 A 目标但 B 目标完全没动。我常用的方法是让 Claude Code 把报错里的“remaining goals”整段复制出来单独作为下一次提示的一部分这样它就能聚焦在当前未完成的部分。第三个坑是一次性输入太多代码。前面也提过AI 的上下文窗口有限你把整个项目的所有细节都塞给它反而会让它“找不到北”。对形式化证明这种严谨任务最优策略是每个会话只处理一个小目标比如“证明某个引理的下界方向”跑通了再开下一个。5.3 省 token 的真实技巧别把大模型当文档传输工具Claude Code 用着爽token 烧得也快。尤其写 Lean 证明这种任务来回报错、反复修改上下文一长费用哗哗的。我总结几个实用的省 token 方式。第一会话及时清理。当一个任务跑完果断用/clear开启新会话别让之前的代码片段一直占着上下文。第二使用/compact压缩会话。当你觉得当前上下文太乱但又不想完全丢失前面的决策信息时可以让 Claude 把整个过程压缩成一份要点摘要能省下不少空间。第三代码提问时只贴差异片段不要整文件复制。比如你只想知道某一行策略怎么改就把那一行和报错贴出来即可。还有一个小技巧是让 Claude Code 先查定理库再写代码。你在提示里加一句“先运行#check确认引理存在再写证明”它就会多执行一次检查避免因为引理名拼错而多走几轮迭代。看起来多了一步实际上节省了后面大量无效往返。6. 后续发展与个人实操体会6.1 下一个大目标新定理、新工具链与新协作模式费马大定理被形式化验证肯定不会是一个终点。按照这个趋势接下来值得关注的方向至少有这三个。第一更多“大定理”会被逐步形式化。费马大定理证明了这套工作流能撑起超大规模证明之后像 L函数与伽罗瓦表示相关的关键模块很可能陆续被社区或者 AI 辅助攻克。第二工具链会越来越自动化。现在 Claude Code 还需要人类在关键节点上介入、设置目标、拆解任务未来可能会出现“证明规划器”这类工具自动把一个巨型定理拆成子任务清单再逐步验证。第三形式化证明的“边界”会突破纯数学进入软件工程、智能体安全和系统验证领域。这次 Clude 官宣的重点词是“机器校验”这个词放到工业界其实就是 CI/CD 里最严格的那种测试——不是跑几个用例而是从逻辑上保证没有漏洞。6.2 我的实际体验哪些能信哪些必须警惕这几天玩下来我最深的体感是当错误信息成为唯一反馈来源时AI 一下就“老实”了。平时跟聊天机器人对话它经常“自信地在错误边缘反复横跳”但在 Lean 环境里编译器说不行就是不行Claude Code 的修正速度和准确率反而比日常写业务代码时更高。这个反差很有意思也让我更相信一件事AI 推理能力要真正兑现需要一套“不给面子”的验收机制。但我还是想给所有打算复现这件事的朋友提个醒别指望 AI 能一步到位生成一个费马大定理的完整证明文件。我自己试过的经验是Claude Code 在简单证明上很稳但一旦目标变得复杂、依赖链条变长它也会“迷失方向”。这时候你需要的是把任务拆小、把报错喂准、把验证跑勤。这跟带一个聪明的实习生干活差不多你越清楚自己要让对方证明什么对方越能发挥出真实水平。形式化证明是慢功夫可它有一个无可替代的好处——只要跑通了每一步都不会骗人。我始终觉得人类和 AI 最好的协作模式不是谁代替谁思考而是让 AI 负责“大胆生成”让机器校验负责“小心求证”。费马大定理这个事件正是这套协作模式第一次站上数学之巅的例证。