数学圈最近刷屏的一件事是菲尔兹奖得主陶哲轩Terence Tao在自己的一线研究中使用 Claude Code 在 Lean 里做形式化证明。消息传开之后很多人把它当成“AI 终于会做数学了”的新闻来读但如果你只停留在这一层就漏掉了背后的技术信号证明正在从一种高度依赖个人智力的活动变成一条“AI 生成候选证明 机器逐条验证”的工程流水线。Claude Code 在这个组合里的角色不是数学家更像一个翻译官和试错员它把自然语言描述的数学命题转换成 Lean 能接受的证明代码读取错误日志再修改再验证。而 Lean 负责当那个不通人情的裁判——每个推理步骤都会被内核逐条检查错一步就编译失败。AI 可以犯错但验证器不会放过任何细节。这种“不确定的生成 绝对严格的验证”组合才是陶哲轩这个案例里最值得普通开发者学习的地方。这篇文章会从陶哲轩的案例切入拆解 Lean 和 Claude Code 分别解决什么问题然后给出完整可复现的工作流搭建 Lean 4 与 Claude Code 环境、用 Claude Code 生成证明代码、用 Lean 验证并迭代修复。同时会覆盖安装和接入模型过程中的常见坑。无论你是关注数学前沿的开发者还是想用 Agent 工具提高复杂任务可靠性的工程师都可以把这篇文章当成一次方法论参考。1. 这件事为什么值得你关注1.1 陶哲轩和“AI 辅助证明”不是新闻噱头陶哲轩的名字不需要太多介绍。作为调和分析、偏微分方程、组合数论等领域都有重量级贡献的数学家他近年来对“形式化数学”表现出了比大多数同行更激进的拥抱态度。从公开材料看他不仅关注 Lean 这样的定理证明器还多次讨论大语言模型与数学研究结合的可能性。这次把 Claude Code 引到 Lean 的工作流里本质上不是一次偶然“尝鲜”而是他持续探索“用工程手段提升数学研究确定性”路线上的自然选择。这件事对普通开发者最直接的冲击不是“大牛也在用 AI”而是当一个人已经站在人类智力金字塔顶端仍然愿意把大量推理验证交给机器说明“AI Agent 严格验证器”的组合在解决高风险、高复杂度任务上已经具备真实生产力。数学证明只是这种任务中最极端、最清晰的一种表现形式。1.2 数学证明正在变成“工程问题”传统数学证明依赖同行评审。一篇论文里的证明往往要经过几个月甚至几年的传播才可能被同行发现漏洞。这里的问题不是审稿人不认真而是人脑在追踪长链条推理时天然有容错阈值。定理越复杂靠人眼挑错的成本越高。Lean 这类形式化证明器改变了这个局面。它把“证明”变成一段可以被机器编译的代码每一个推理步骤都要符合内核预设的规则。一旦你写出一个被 Lean 接受的证明这个定理的正确性就不再依赖审稿人的主观判断而是可以被任何一台安装 Lean 的机器重新验证。陶哲轩和他的合作者在大量工作中推进的正是这种把数学结论变成“可验证产物”的工程化过程。维度传统证明Lean 形式化证明验证方式同行审阅依赖专家判断机器逐条检查推理规则错误发现时机可能数月或数年后编译期立即暴露可复用性证明依赖“讲故事”证明像代码一样被引用和组合AI 参与度几乎无法介入大模型可直接生成证明片段1.3 对普通开发者的意义如果你不做数学这件事还有参考价值吗有。Claude Code 本质上不是“数学专用工具”而是一个命令行 AI Agent。它能读写文件、执行命令、查看错误日志、围绕任务多轮迭代。这和你在后端项目里用 AI 做重构、修复编译错误、补充单元测试是同一类能力。陶哲轩示范的是“如何让 AI 承担大量试错工作同时用自动化工具守住正确性底线”。这个模式可以平移到你自己的项目里AI 负责快速生成候选实现测试和编译器负责严格把关。理解了这一点你再看“AI 写代码”这件事就不会只关心它补全得快不快而是会关心怎么搭一条让 AI 输出被验证的流水线。2. 基础概念Lean 和 Claude Code 各自解决什么问题2.1 Lean不是编程语言而是“证明编译器”很多人第一次听到 Lean会以为它是一个数学计算软件像 Mathematica 或者 MATLAB。这个理解需要纠正。Lean 是一个基于依赖类型论的交互式定理证明器它在数学界的地位更像“证明编译器”你写下一个数学命题和证明步骤Lean 会逐条检查证明步骤是否严格符合逻辑规则。Lean 之所以能对数学界产生吸引力一部分原因是它的数学库 Mathlib 已经非常庞大。从自然数到群论、拓扑、测度大量现代数学对象都已经被形式化。数学家用 Lean 做证明不是重新发明轮子而是在一个已经铺好大量地基的层次上继续盖楼。新的证明如果成立就会像积木一样被累加到 Mathlib 中供后来者引用。这里真正容易误解的地方是Lean 不是自动定理证明器。它不会在输入一个命题后自动给你答案。它更像一个严格的编译环境你需要“写出证明”它负责“检查证明”。不过当大语言模型加入之后这个“写证明”的环节就可以被部分自动化了。2.2 Claude Code不是聊天框是能操作项目的 AgentClaude Code 是 Anthropic 推出的命令行编程代理。它和网页版聊天窗口最大的区别在于“行动能力”和“上下文”。Claude Code 在你项目目录下启动后可以读取项目文件、执行 shell 命令、查看报错信息、调用构建工具然后根据结果决定下一步。它不再只是“给你建议”而是可以参与完整的工程循环。对 Lean 项目来说Claude Code 尤其有价值的一点是Lean 的编译错误信息往往非常具体会告诉你哪个类型不匹配、哪个目标没有被证明、哪个标识符不存在。Claude Code 可以把这些错误当作反馈信号反复修改证明代码直到 Lean 不再报错。这个过程已经相当接近一个初级证明工程师的工作方式。2.3 为什么这两个工具组合在一起特别有力量单独看Claude Code 的生成能力很强但可能产生幻觉单独看Lean 的验证能力很强但不会自己创造证明。两者的结合构成了一个经典工程模式生成器负责发散验证器负责收敛。能力Claude CodeLean生成证明片段强弱不会主动创造验证推理合法性弱可能出错强逐条规则检查读取并理解报错强无上下文理解强能理解自然语言仅理解类型和证明状态在这种模式下人类数学家真正要做的只剩下最高层的任务提出正确的命题、判断证明方向是否合理、拆解证明思路。剩下的大量机械化试错交给 Claude Code正确性把关交给 Lean。3. 环境准备搭建 Lean 4 与 Claude Code 的开发环境3.1 安装 Lean 4 与 elanLean 的工具链管理工具是 elan相当于 Rust 社区的 rustup。它负责安装和切换 Lean 版本。安装方式以官方文档为准常见做法是通过脚本安装# macOS / Linux 常见安装方式 curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash # 安装后让 elan 进入当前 shell source $HOME/.elan/env # 设置使用稳定的 Lean 4 工具链 elan default stable需要注意的一点是安全起见安装脚本的 URL 请以 Lean 官方文档为准不要从非官方渠道获取脚本避免供应链风险。安装完成后可以用下面的命令验证lean --version如果输出了类似Lean (version 4.x.x)的版本信息说明 Lean 本体已经安装成功。3.2 创建 Lean 项目Lean 项目通常使用 lake 作为构建工具它的功能和 cargo、maven 类似。初始化一个项目很简单lake new my_math cd my_math项目创建后目录结构大概是这样的my_math/ ├── lakefile.lean ├── lean-toolchain ├── MyMath/ │ └── Basic.lean └── Main.leanMyMath/Basic.lean是放证明代码的地方。第一次运行lake build时如果项目引入了 Mathlib会触发 Mathlib 的下载和编译这个过程可能非常漫长需要保持耐心。如果只是想验证单个文件也可以跳过整个项目构建。3.3 安装 Claude CodeClaude Code 最常见的安装方式是 npm 全局安装也可以使用官方安装脚本。两种方式任选一种# 方式一通过 npm 全局安装 npm install -g anthropic-ai/claude-code # 方式二官方安装脚本以官方文档为准 curl -fsSL https://claude.ai/install.sh | bash安装完成后执行claude --version验证是否成功。如果终端提示找不到命令多半是 Node 环境或全局安装路径没有加入 PATH需要重新配置环境变量后重启终端。3.4 配置模型访问Claude Code 在启动时需要一个可用的模型访问通道。使用 Anthropic 官方 API 时可以通过环境变量配置密钥export ANTHROPIC_API_KEY你的密钥然后进入项目目录启动 Claude Codecd my_math claude这里需要特别提醒不要把 API 密钥写进任何会提交到 Git 仓库的文件里也不要把密钥写进 CLAUDE.md。正确做法是通过环境变量或团队内部的密钥管理平台注入。关于模型接入不少开发者会通过第三方 API 网关接入其他模型。这类方式最大的坑在于模型名映射。如果 Claude Code 上报类似xxx is not a model this version of claude code recognizes的错误通常意味着网关侧配置的模型名和 Claude Code 期望的模型名不一致。这类问题没有灵丹妙药优先检查网关映射名并确认 Claude Code 版本是否过旧。3.5 在 VS Code 中配合使用Claude Code 本身以命令行交互为主但很多开发者更习惯在 IDE 里工作。VS Code 可以通过集成终端直接运行claude也可以配合相关插件获得更好的体验。核心原则是Claude Code 需要能访问当前项目目录这样它才能读取文件、修改文件并执行构建命令。在 Lean 项目中使用 Claude Code 时建议始终从项目根目录启动不要从子目录启动否则它无法正确感知lakefile.lean和lean-toolchain的上下文。4. 核心工作流从自然语言到机器验证的闭环4.1 工作流四步循环陶哲轩用 Claude Code 在 Lean 中做形式化证明外界看起来很神秘拆开看其实就是四步循环用自然语言描述要证明的命题。让 Claude Code 生成 Lean 证明代码。用 Lean 编译验证得到错误反馈。把错误反馈给 Claude Code循环修复直到验证通过。这个循环的关键不在于每一步多复杂而在于“验证”环节是绝对严格、不可能被糊弄过去的。AI 可以犯错但 Lean 会把错误精确地抛回给你。4.2 第一步把命题写成精确的自然语言给 Claude Code 提要求时最忌讳的是只说“帮我证明某个数学结论”。Lean 要求精确的类型签名所以你需要把命题写清楚。比如要证明“对任意自然数 nn 0 n”不能只写“证明 n0n”而要写清楚约束条件n 是什么类型结论是什么表达式。更好的做法是直接在提示词里给出 Lean 的定理声明。例如请证明下面的 Lean 定理 theorem add_zero_right (n : Nat) : n 0 n : by sorry把sorry背后的证明补全。sorry在 Lean 里是一个占位符表示“这个证明还没写”Claude Code 看到它就知道任务目标在哪里。4.3 第二步让 Claude Code 生成证明代码在项目目录下启动 Claude Code 后可以给出类似下面的指令打开 MyMath/Basic.lean补全 theorem add_zero_right (n : Nat) : n 0 n 的证明。 完成后用 lake env lean MyMath/Basic.lean 验证。只有验证通过才算完成。 注意不要修改其他定理。这里有几个细节值得注意。第一要告诉 Claude Code 用什么命令验证第二要让 Claude Code 直接读文件、写文件而不是只输出一段代码第三要明确限定修改范围防止它顺手改动无关内容。从实践看限定越清楚Claude Code 越不容易跑偏。4.4 第三步用 Lean 验证并收集错误Claude Code 生成证明后运行验证命令lake env lean MyMath/Basic.lean如果没有任何输出退出码为 0说明证明已经通过。如果输出错误Lean 会给出非常具体的信息哪个文件哪一行、哪个标识符不存在、哪个类型不匹配、还有哪些目标没有被证明。这些信息就是 Claude Code 下一轮迭代的输入。4.5 第四步批量修复不如逐个修复一个常见误区是把一整页错误信息一次性扔给 Claude Code让它“帮我全部修好”。实践下来更稳妥的做法是让 Claude Code 一次只解决一个错误。因为 Lean 的错误经常像多米诺骨牌——第一个错误会引发后续一连串连锁报错当你把第一个错误的上下文修对之后后面的错误可能自动消失。所以建议让 Claude Code 每次拿到最新的错误信息后首先分析“根因错误”和“衍生错误”只处理根因然后重新编译用新的错误信息继续迭代。这个习惯在普通开发里修编译错误时同样适用。5. 完整示例让 Claude Code 在 Lean 中证明一个定理5.1 项目文件结构一个适合演示的 Lean 项目结构如下my_math/ ├── lakefile.lean ├── lean-toolchain ├── MyMath/ │ └── Basic.lean └── CLAUDE.md其中CLAUDE.md是写给 Claude Code 看的项目说明相当于给 Agent 的一份“入职手册”。5.2 配置 CLAUDE.md# Lean 4 项目上下文 ## 项目介绍 这个项目用于演示如何使用 Lean 4 进行数学定理的形式化证明。 ## 常用命令 - lake build编译并验证全部代码 - lake env lean MyMath/Basic.lean单独验证某个文件 - 在 Lean 环境中输入 #check 定理名 查看定理类型 ## 代码规范 - 所有定理必须通过 lake build 验证 - 优先使用标准策略simp、omega、positivity、nlinarith - 导入 Mathlib 的语句放在文件最前面 - 不要修改与当前任务无关的定理CLAUDE.md 的价值在于每次 Claude Code 进入项目都会自动读取这份项目上下文。它可以避免 Claude Code 在多次会话之间反复猜测项目规范也方便团队成员共享同一套约束。5.3 示例任务在 Lean 中证明几个基础定理我们把下面这段 Lean 代码放入MyMath/Basic.leanimport Mathlib -- 定理1自然数 n 满足 n 0 n theorem add_zero_right (n : Nat) : n 0 n : by simp -- 定理2自然数加法满足交换律 theorem add_comm_example (a b : Nat) : a b b a : by omega -- 定理3整数的平方非负 theorem square_nonneg (x : Int) : 0 x * x : by positivity如果这些证明不是你自己写出来的而是由 Claude Code 根据自然语言命题生成的那么你的工作流已经和陶哲轩案例的核心思路一致了人负责提出命题和判断方向AI 负责补全证明细节Lean 负责最终裁决。5.4 通过 Claude Code 让证明落地如果要从零开始给 Claude Code 的提示词可以是这样请在 MyMath/Basic.lean 中写下并证明以下三个定理 1. 对任意自然数 n有 n 0 n 2. 对任意自然数 a b有 a b b a 3. 对任意整数 x有 0 x * x 每个定理都要给出完整的 Lean 4 代码并且通过 lake env lean MyMath/Basic.lean 验证。 请先把文件当前内容读出来再决定如何修改。当 Claude Code 完成后你只需要检查最终代码和验证结果。这就是最简版本的“AI 生成证明 机器验证”闭环。5.5 代码逻辑解读上面三个定理对应三种不同的证明策略对刚接触 Lean 的读者很有参考价值。theorem add_zero_right (n : Nat) : n 0 n : by simp中simp策略会自动调用 Mathlib 中已有的引理比如Nat.add_zero把n 0化简为n。这里容易踩的一个坑是如果你把simp改成rfl证明会失败。原因是rfl只能处理定义上相等的目标而n 0 n在 Lean 的自然数加法定义下并不是定义上直接相等它需要借助Nat.add_zero这个引理。theorem add_comm_example (a b : Nat) : a b b a : by omega中omega是一个针对线性整数和自然数算术的自动化决策过程。它可以直接处理加法交换这种在自然数上看似平凡、但需要归纳支持的命题。theorem square_nonneg (x : Int) : 0 x * x : by positivity中positivity策略专门用于证明目标表达式非负。数学上整数平方非负是基本结论但在 Lean 里你需要选对策略才能把这条结论转化成机器可接受的证明。需要注意的是Mathlib 版本会持续演进个别策略在不同版本中的行为可能有细微差异。如果你的本机环境里某个策略不可用或者报错可以换成更基础的写法例如对a b b a使用exact Nat.add_comm a b对0 x * x使用exact Int.mul_self_nonneg x。这里没有黑魔法验证器会诚实地告诉你哪种写法不成立。6. 运行结果与效果验证6.1 运行验证命令在my_math项目根目录执行lake env lean MyMath/Basic.lean echo exit code: $?如果三个定理都证明成功终端不会打印任何错误信息退出码为 0。这和普通编程语言“编译通过”的含义不同Lean 的编译通过意味着所有证明步骤都已经被内核验证。6.2 如何判断证明真的被验证除了退出码还可以在 Lean 的交互环境里用#check命令检查定理的存在lake env lean进入 Lean 交互环境后输入#check add_zero_right #check add_comm_example #check square_nonneg如果定理已经进入环境Lean 会打印出这些定理的类型add_zero_right (n : Nat) : n 0 n add_comm_example (a b : Nat) : a b b a square_nonneg (x : Int) : 0 x * x看到这种输出说明这些定理不再是“你写在纸上的想法”而是可以被后续代码引用的、经过机器验证的数学事实。6.3 失败时先看哪里如果lake env lean报错不要急着把整个错误信息丢给模型。先定位错误信息的头部那里通常会给出文件名、行号和列号。然后再看错误类型常见的有unknown identifier找不到某个名称可能是拼写错误也可能没有导入对应的 Mathlib 模块。type mismatch类型不匹配说明证明步骤没有对齐目标或者前提引理用错了。unsolved goals证明没有覆盖所有子目标还有证明义务没有完成。把这些信息读一遍再决定是让 Claude Code 继续修还是手工调整方向。把错误信息完整、原样地贴给 Claude Code往往比你自己猜半天更高效。7. 常见问题与排查思路问题现象可能原因排查方式解决方案输入claude提示command not foundNode 环境或 PATH 未配置检查npm root -g和 PATH重新安装或把全局安装目录加入 PATH然后重启终端启动报failed to run claude code: error: could not locate the claude cli on path没有找到 Claude CLI 可执行文件用which claude检查路径用官方安装脚本安装或把 CLI 所在目录加入 PATH接入第三方模型时报xxx is not a model this version of claude code recognizes模型名映射与客户端期望不一致检查网关配置和 Claude Code 版本更新 Claude Code 版本或在网关侧把模型名映射为客户端能识别的名称Lean 报unknown identifierMathlib 未导入或名称拼写错误搜索 Mathlib 文档确认名称在文件开头添加import Mathlib并修正拼写simp无法证明某些等式目标涉及的定义或引理不在简化器视野内查看目标是否满足定义相等改用rw、omega、exact等更精确的策略首次lake build耗时极长需要下载并编译 Mathlib观察网络和 CPU 资源占用耐心等待或使用带 Mathlib 缓存的开发环境Windows 终端中文乱码终端编码与 UTF-8 不一致在终端执行chcp查看代码页执行chcp 65001切换到 UTF-8想彻底卸载 Claude Code全局安装残留查看