最近陶哲轩使用 Claude Code 在 Lean 中做形式化证明的消息同时击中了数学圈和 AI 编程圈。如果只看表面这是一位著名数学家尝试新工具但放在过去几年形式化证明的发展脉络里看这件事真正指向的变化是长期靠人肉翻译和调试的形式化证明工作流正在被 AI Agent 改造成一个有反馈、可迭代的协作闭环。我的核心判断是Claude Code 这类工具在数学证明和日常编程里的价值并不是“一键生成正确结果”而是把大量重复、琐碎、需要逐轮试错的机械劳动变成人和 AI 之间高频率的反馈循环。工具能做多少取决于你的任务有没有明确的评判信号。Lean 恰好是个极端例子——编译通过就是通过任何一步不成立就过不去。这种环境一旦接上 Agent迭代效率的提升会非常明显。这篇文章不打算复述新闻而是想沿着这条线拆清楚三件事为什么 AI 辅助形式化证明是一个比“AI 写代码”更值得关注的信号Claude Code 到底怎么装、怎么配、怎么用以及你能从这件事里迁移到日常开发工作流的方法论。1. 陶哲轩在 Lean 里用 Claude Code为什么值得程序员关注1.1 Lean 和形式化证明到底在解决什么问题先说形式化证明。很多人把它理解成“让计算机自动证明数学定理”这个理解不完全对。更准确地说形式化证明是人和计算机协作把一条自然语言证明拆成机器可以逐步验证的符号推导。Lean 就是这样一个交互式定理证明器你写下一个数学命题然后逐步写证明步骤Lean 会检查你的每一步推导是否严格成立任何一步站不住脚都会变成编译错误反馈回来。这听起来像一个加分项实际上在数学研究里长期以来是一道很高的门槛。自然语言证明可以省略“显然”、可以依赖读者的背景知识而形式化证明不能。把一页纸的证明变成 Lean 里的几百行甚至几千行代码是常态。大量精力不是花在“想清楚证明思路”而是花在“如何把这个思路翻译成 Lean 能接受的形式”以及“为什么这个库函数调用又不对”。过去几年Lean 社区的成长很大程度上靠人力堆出来。一个大型数学库比如社区里持续维护的 mathlib就是由大量贡献者一点一点把数学结论形式化进去的。每一步都要人工完成很慢很枯燥也因此只有少数愿意接受这种工作方式的数学家能坚持下来。陶哲轩在这次尝试里用 Claude Code 做形式化证明之所以引起讨论我理解不是因为 AI 一次性完成了某个惊天动地的证明而是它让“翻译和调试”这个最消耗人力的环节第一次有了真正可用的自动化。1.2 Agent 工具改变了“翻译和调试”环节如果把传统 AI 代码补全工具比作“一个很会接茬的输入法”那 Claude Code 这类 Agent 工具就更像一个“能自己打开文件、运行命令、读报错然后修改代码的实习生”。它不是一个只生成文本的模型而是一个能围绕任务操作环境的代理。在 Lean 形式化证明里这个差异被放大得很明显。证明过程中AI 生成的代码经常不能一次通过。以前你需要在编辑器、终端、文档之间来回切换把报错信息复制出来思考下一步怎么改现在可以把整个项目目录交给 Agent让它自己去读 Lean 文件、运行检查、读取报错、修改代码你只负责在关键时刻给出方向。不要把这个过程理解成“程序员失去工作”或“数学家失去价值”。它恰恰相反。当大量机械性的翻译和调试被接管后人被解放出来做更重要的事判断证明思路是否成立、决定拆成哪些引理、审查最终结果是否正确。这个分工模式比“AI 直接给出答案”更接近真实的生产协作。2. 从零跑通 Claude Code安装、启动与最小可用流程2.1 想清楚再从哪个入口进入网上关于 Claude Code 的讨论很多有说 CLI 的有说 VSCode 插件的也有说桌面版的。先别急着装想清楚你的使用习惯。Claude Code 底层的 Agent 工作流是同一套CLI、桌面端、VSCode 插件只是不同的外壳。CLI 适合本来就习惯终端、希望在任意目录快速启动的人VSCode 插件适合把 AI 嵌入编辑器边读代码边让它改桌面端则提供一个独立界面适合不想和终端打交道的人。如果你是为了跟风体验我的建议很简单先用 CLI 跑通最小流程。它的依赖最少反馈最直接也最容易排查问题。等确认它能正常工作再决定要不要换成桌面端或编辑器插件。直接一上来装三个入口一旦出了问题你会不知道问题是出在配置还是外壳上。还要注意一个前置条件Claude Code 是一个会读取本地文件、执行命令的工具在安装前先想好你会在哪些项目目录里使用它。不要在一个没有 git 历史、没有明确任务边界、满是敏感信息的目录里随意让它操作。这个问题后面会专门展开。2.2 安装和初次认证安装方式在不同版本里会有细节差异最通用的路径是使用 npm 全局安装。以下是常见写法具体命令以你当前下载的官方文档为准npm install -g anthropic-ai/claude-code claude --version如果安装成功claude --version能打印出版本号。如果报错说找不到命令通常不是安装失败而是 npm 的全局 bin 目录不在 PATH 里。可以先用npm bin -g查看全局 bin 路径再把它加入 PATH。很多 Windows 上的用户还会在 VSCode 插件里遇到could not locate the claude cli on path这种报错本质上也是同一个问题插件启动 CLI 时PATH 里没有包含它。首次启动claude一般会进入认证流程。根据你使用的版本可能是用浏览器登录 Claude 账号也可能是设置 API Key 环境变量。无论哪种方式我建议把认证信息放在环境变量里而不是写进项目文件避免把密钥提交到 git 仓库。这里有一个常见的误区有些人看到教程里说“修改 settings.json 可以接入其它模型”就立刻去找配置文件结果改完发现根本没生效。原因多半是版本不认、配置位置不对、或者模型名拼写不匹配。后面第 3 章会专门展开。注意安装和使用前先确认 node、npm 的版本满足工具要求。如果安装过程中出现权限错误也不要直接改用 root 或管理员模式运行优先处理目录权限问题。2.3 最小可用流程先完成一个能验证的小任务很多教程会用非常宏大的案例来演示 Claude Code比如“让它生成一个完整项目”。但真实上手时我更建议从一个极小的任务开始。具体步骤可以是新建一个临时目录放一个简单的文本文件或一个最小的代码工程。在目录里运行claude先让它列出目录结构、解释文件内容。给它一个非常具体、可验证的小任务比如“帮我写一个函数输入一个数字列表返回去重后的列表”。让它运行测试或执行脚本观察它是否会自己读取结果、修正错误。任务完成后查看它的日志和修改记录确认它没有做超出任务范围的操作。这一步看起来简单但很重要。你会快速搞清楚三件事这个 Agent 是怎么理解你的指令的它能不能自己从错误中恢复它会不会悄悄做你没让它做的事情。后面两件事决定了你是否愿意在更复杂的 Lean 证明任务里信任它。3. 模型接入与配置决定上限的不是模型而是配置边界3.1 官方模型、第三方兼容接口、本地部署要分别对待搜索 Claude Code 使用教程热度很高的一个问题是怎么接入第三方模型比如 DeepSeek、智谱这些。这个需求很合理不是每个人都有可用的官方 API 额度或者团队内部已经有自己的模型网关。但需要先把三种情况分清楚。第一种是使用官方模型和官方认证流程。这是风险最小、兼容性最好的方式。你只需要保证认证信息正确、网络可达、模型名称符合当前版本的约定。第二种是通过兼容接口接入第三方模型。社区常见的做法是通过环境变量或配置文件把请求地址指向第三方模型供应商提供的兼容端点并填上对应的模型名和认证 Token。这种方案的可用性很大程度上取决于三个因素当前 Claude Code 版本对接口协议的兼容程度、第三方模型是否完整支持 Agent 所需的工具调用能力、你的使用方式是否符合供应商的服务条款。第三种是本地部署模型比如通过本地方案跑一个模型然后提供兼容接口。这种方式对算力、内存和显存要求高而且很多本地小模型在长上下文、工具调用和多轮迭代上表现不稳定。如果只是学习可以把它当作一个实验如果要做正经的 Lean 证明或生产项目先把期望降到最低。要特别提醒无论你接入哪种模型都要遵守对应平台和服务商的使用条款不要把工具用到灰色地带。模型能力、报错提示和接口行为在不同版本里变化很快网上教程常常过时。3.2 关键参数和常见报错在实际使用中最影响体验的往往不是模型本身的强弱而是配置边界。以下是几个高频问题以及排查动作现象常见原因排查动作启动时提示could not locate the claude cli on pathPATH 中没有包含 CLI 所在目录用npm bin -g查看路径并把该目录加入 PATHVSCode 插件场景需要重启编辑器提示某个模型名不被当前版本识别模型名拼写不对、接口不兼容或版本不支持核对模型名拼写、查看当前版本支持哪些模型、确认接口地址是否正确修改 settings.json 后不生效配置位置不对、格式错误或版本不读取该字段先确认配置文件位置和官方文档字段名修改后重启进程再测试中文输出乱码终端编码与 UTF-8 不一致在 Windows 终端把代码页切到 UTF-8或更换终端软件API Key 鉴权失败Key 无效、过期、环境变量命名错误检查环境变量名和值确认网络能到达对应 API 端点这些报错看起来杂其实都指向同一个排查思路先分清楚是“安装层”“配置层”还是“模型层”出了问题。不要一上来就重装工具也不要反复更换模型供应商。先确认最基本的一条路径能不能跑通再逐步叠加配置。3.3 按使用深度把配置分成三层同样是安装 Claude Code不同人的配置深度完全不同。我把常见的配置要求分成三个层级尝鲜层只在临时目录里跑通一个简单任务使用官方模型和默认配置即可不需要额外调参数。这一层的目的是建立体感。日常层确定固定的模型和接口配置好常用项目目录把模型名、工作目录、输出路径、上下文长度这些关键参数固定下来。建立自己的任务模板让 Agent 每次开工前先读项目说明文件。工程化层把 Agent 使用纳入真实项目的开发或证明流程。你需要考虑任务记录、日志留存、权限控制、批量执行策略、失败重试、版本兼容和成本控制还要约定什么任务可以交给 Agent 自动执行什么任务必须人工确认。这也是为什么我不建议一上来就追求高级配置。先跑通再固化最后工程化。顺序反了大概率会把自己淹没在层出不穷的报错里。注意涉及第三方接口或本地部署时先确认是否符合服务条款和合规要求。技术能力是手段使用边界是底线。4. 把证明拆给 Claude Code一个可复用的五步工作法4.1 为什么形式化证明适合做成 Agent 流程Claude Code 能做的项目管理、代码解释、日志分析等事情其它工具也能做。但 Lean 形式化
)