1. 为什么要在 Lean 4 里接 DeepSeek-Prover-V2-671B如果你正在做数学定理自动证明Lean 4 基本绕不开。它把数学命题写成可被机器检查的代码证明对不对由内核说了算而不是靠人眼看。问题在于写 Lean 4 证明本身门槛不低theorem ... : by sorry之后那一大段 tactic 怎么补往往比理解定理还费劲。DeepSeek-Prover-V2-671B 就是冲着这个环节来的——它是一个专为 Lean 4 形式化证明训练的超大垂直领域语言模型输入一段带sorry的定理骨架它能给出证明计划加可编译的 tactic 代码。这个模型适合谁一类是数学/形式化方向的研究者想批量跑 MiniF2F、ProverBench 这类基准另一类是工程团队想把定理证明能力接进自己的题解平台或 AI 助教。它的能力边界也很清楚擅长竞赛题和教材级定理遇到真正前沿的开放问题仍然会卡住所以把它当成“高强度补全助手”而不是“自动数学家”更实际。我试过的典型流程是本地装好 Lean 4 和 Mathlib把定理写成标准骨架通过统一 API 通道把骨架发给 Prover-V2拿回证明代码后直接lake build验证。整条链路里最烦的其实不是模型而是环境配置和 API 接入的琐碎细节。下面按“环境 → 接入 → 配置 → 验证 → 排障”的顺序拆开讲配置骨架可以直接复制。2. Lean 4 与 Mathlib 环境准备Lean 4 的工程管理靠elan版本管理器加lake构建工具。不要手动去下二进制用官方脚本最省事。装完之后确认版本Prover-V2 生成的代码通常针对较新的 Mathlib版本太旧会出现大量unknown identifier。# 安装 elanLean 版本管理器 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh source $HOME/.elan/env # 确认安装 lean --version lake --version接着建一个带 Mathlib 依赖的工程。Mathlib 首次拉取体积很大建议预留时间和磁盘lake new prover_demo cd prover_demo # 在 lakefile 中加入 Mathlib 依赖Lean 4 新版用 lakefile.toml cat lakefile.toml EOF [[require]] name mathlib scope leanprover-community EOF # 拉取依赖并缓存编译结果 lake update lake exe cache getlake exe cache get这一步很关键。Mathlib 全量编译在普通机器上要几个小时用官方缓存能压到几分钟。如果这步失败多半是网络或缓存服务器临时问题重试即可不要直接lake build硬编。验证环境是否可用写一个最小定理import Mathlib theorem demo_add : (1 : ℕ) 1 2 : by norm_numlake build通过就说明 Lean 4 Mathlib 这条链路通了。接下来才是把模型接进来。3. 通过 TaoToken 统一 API 接入 Prover-V2本地直接跑 671B 权重对绝大多数人是不现实的显存需求摆在那。更实际的做法是走 API。TaoToken 提供统一的 Key 和 API 通道好处是你不用为每个模型单独维护一套鉴权和地址换模型只改一个字段。对 Prover-V2 这种垂直模型来说统一通道能省掉不少对接成本。先拿 Key进入控制台创建 API Key地址是 https://taotoken.net/api-keys?utm_sourcetaotoken_aicg_blog_endutm_contentapi_keysutm_campaignrewrite 。创建后复制保存页面只显示一次。接入文档在 https://taotoken.net/doc?utm_sourcetaotoken_aicg_blog_endutm_contentdocutm_campaignrewrite 参数细节以文档为准。API 基地址统一用 https://taotoken.net/api 注意这个地址不带任何查询参数。请求格式兼容 OpenAI 风格的/v1/chat/completions所以现有的 SDK 基本能直接复用只要把base_url和api_key换掉。一个容易踩的坑Prover-V2 的输出是 Lean 4 代码里面包含大量反引号和花括号用 shell 拼接 JSON 极易出错。建议用 Python 或直接写 JSON 文件别用curl手拼字符串。4. 可复制的 config.toml 与 settings.json 骨架很多工具链编辑器插件、Agent 框架、本地代理都靠config.toml或settings.json读模型配置。下面给两份骨架字段名按常见约定写你按自己工具的文档微调即可。config.toml适合命令行工具或 Agent 框架# config.toml [provider] name taotoken base_url https://taotoken.net/api api_key_env TAOTOKEN_API_KEY # 从环境变量读取别硬编码 [model] id deepseek-prover-v2-671b max_tokens 8192 temperature 0.2 # 证明任务要稳温度压低 top_p 0.95 [request] timeout 300 # 长证明生成慢超时给足 retry 2settings.json适合编辑器插件类工具{ models: [ { name: prover-v2, provider: taotoken, baseUrl: https://taotoken.net/api, apiKey: ${TAOTOKEN_API_KEY}, model: deepseek-prover-v2-671b, maxTokens: 8192, temperature: 0.2 } ], defaultModel: prover-v2 }Key 一律走环境变量别写进文件再提交到仓库export TAOTOKEN_API_KEY你的Key温度这块值得多说一句。数学证明要求确定性temperature设 0.2 左右比较合适设太高模型会“发挥”生成的 tactic 看着合理但编译不过。max_tokens给到 8192是因为复杂定理的证明计划加代码很容易超过 2000 token截断了就白跑。5. 验证请求与成功结果配置好之后先做一次最小验证确认通道通、模型能返回 Lean 4 代码。用 Python 发一个请求把定理骨架塞进去import os from openai import OpenAI client OpenAI( base_urlhttps://taotoken.net/api/v1, api_keyos.environ[TAOTOKEN_API_KEY], ) formal_statement import Mathlib import Aesop set_option maxHeartbeats 0 theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) 10 : by sorry .strip() prompt fComplete the following Lean 4 code: lean4 {formal_statement}Before producing the Lean 4 code, provide a detailed proof plan outlining the main steps and strategies. .strip()resp client.chat.completions.create( modeldeepseek-prover-v2-671b, messages[{role: user, content: prompt}], max_tokens8192, temperature0.2, )print(resp.choices[0].message.content)成功返回的内容通常分两段先是一段自然语言的证明计划说明用哪些引理、怎么化简然后是一段 lean4 代码块把 sorry 替换成真正的 tactic。把代码块里的内容贴回 .lean 文件lake build 通过就说明整条链路跑通了。 如果只是想先在线体验一下模型输出风格不想配环境可以直接用模型对话入口https://taotoken.net/model-chat?utm_sourcetaotoken_aicg_blog_endutm_contentmodel_chatutm_campaignrewrite 。把定理骨架贴进去看它给的证明计划是否符合预期再决定要不要接进工程。 ## 6. 微调数据集准备与验证动作 如果你要做领域微调比如针对某类教材或竞赛题风格数据集格式要和 Prover-V2 的训练格式对齐。核心是“形式化语句 证明”成对出现最好再带上推理链。ProverBench 是个很好的参考集325 道题覆盖 AIME、微积分、数论、代数、概率、抽象代数等方向可以拿它做评测基线。 数据准备的基本结构每条样本长这样 json { formal_statement: import Mathlib\n\ntheorem foo : ... : by\n sorry, proof: theorem foo : ... : by\n norm_num, plan: 先用 norm_num 化简再处理绝对值... }准备流程分三步。第一步把原始题目转成 Lean 4 骨架确保import和类型标注正确这一步错了后面全白搭。第二步用 Prover-V2 批量生成证明把能通过lake build的留下编译失败的丢弃或人工修。第三步把通过的样本连同证明计划一起整理成训练格式。验证动作不能只看 loss。微调后必须跑一遍编译通过率拿一批留出的定理让微调后的模型生成证明统计lake build成功比例。这个指标比任何训练曲线都实在。另外注意上下文长度Prover-V2 支持到 163K token但微调时序列太长会显著吃显存建议按实际定理长度裁剪别盲目拉满。7. 本篇常见错排查报错unknown identifier norm_numMathlib 没加载或版本不匹配。检查文件顶部有没有import Mathlib以及lake update是否成功。Prover-V2 生成的代码默认依赖较新 Mathlib版本旧了会大面积报错。API 返回 401 或鉴权失败Key 没设进环境变量或者base_url写错。注意基地址是https://taotoken.net/apiSDK 里通常要补成https://taotoken.net/api/v1具体以接入文档为准。Key 前后别带空格。返回内容被截断代码块不完整max_tokens太小。复杂定理的证明计划加代码轻松超过 4000 token调到 8192 甚至更高。截断的代码贴回去必然编译失败。生成的证明编译超时Lean 里set_option maxHeartbeats 0可以关掉心跳限制但有些 tactic 本身就会跑很久。可以在骨架里加set_option maxHeartbeats 400000给一个上限避免单个定理卡死整个构建。lake exe cache get失败缓存服务器临时不可达重试几次。实在不行再lake build但要接受长时间编译。别在缓存没拉全的情况下就断定环境坏了。温度设太高导致证明“看着对但过不了”把temperature降到 0.2 以下证明任务不需要创造性发散。如果还是不稳检查top_p是否过高。8. 长期编码与 Agent 场景的接入建议如果你不是偶尔跑几个定理而是要把 Prover-V2 接进长期的编码流程或 Agent 系统比如自动题解平台、批量基准测试、CI 里自动补证明那按次调用 API 的方式在成本和稳定性上都不划算。这种场景更适合用 Coding Plan 这类长期方案把模型通道固定下来省去每次手动配 Key 的麻烦https://taotoken.net/coding-plan?utm_sourcetaotoken_aicg_blog_endutm_contentcoding_planutm_campaignrewrite 。接入时有两个工程细节值得注意。一是把 Lean 编译验证做成独立步骤模型返回的代码先落盘再lake build编译失败的样本自动记录方便后续分析模型在哪些题型上容易翻车。二是给请求加超时和重试长证明生成偶尔会慢超时设 300 秒比较稳妥重试 2 次足够。最后提醒一句Prover-V2 再强也只是补全工具Lean 4 内核才是最终裁判。任何生成的证明都必须过编译别因为模型说得头头是道就跳过验证。把编译通过率当成唯一硬指标这条链路才靠得住。