Seed Prover 1.5：基于Agentic架构的可调试Lean推理操作系统

1. 项目概述Seed Prover 1.5 不是“又一个数学模型”而是一套可复现、可调试、可进化的 Lean 推理操作系统你有没有试过在 Lean 中写一个简单的add_comm证明结果卡在第三行反复修改rw和simp的顺序最后发现是 mathlib 版本不匹配或者更糟——你花两小时写完的证明在同事的机器上跑不通报错信息里全是unknown identifier real.sqrt这不是你代码的问题而是整个形式化数学工作流长期存在的“黑箱困境”模型输出一串 Lean 代码能跑通就谢天谢地跑不通就只能靠人肉二分排查。Seed Prover 1.5 的核心价值恰恰在于它把这套黑箱彻底拆开、摊平、标上刻度变成一个工程师能理解、能干预、能优化的系统。它不是用更大的模型堆出更高分数而是用一套全新的“Agentic 架构”重构了整个推理链路——从问题输入、策略生成、工具调用、状态缓存到失败回溯全部暴露在开发者视野之下。关键词Seed Prover、Agentic、Lean、mathlib、Python这五个词组合起来描述的不是一个静态模型而是一个以 Python 为胶水、以 Lean 为执行引擎、以 mathlib 为知识底座、以 Agentic 范式为控制逻辑的动态推理操作系统。它面向的不是“想学定理证明”的初学者而是“正在用 Lean 做研究”的数学工作者、形式化验证工程师、AI4Math 领域的研究者以及那些厌倦了“模型输出即真理”、渴望真正掌控推理过程的技术实践者。如果你的目标是快速跑通一个 Putnam 题目它能给你 9 小时内 11/12 的结果但如果你的目标是搞懂“为什么这道题它用了 17 次 mathlib 搜索却只调用了 3 次 Python”那 Seed Prover 1.5 才是你真正该深入的项目。它把过去藏在 RL 训练日志里的隐性知识变成了你在 VS Code 里就能单步调试的显性流程。2. 核心架构拆解Agentic 架构的本质是让模型学会“像人类数学家一样做决策”2.1 为什么必须抛弃“一步到位”的 Whole-Proof 模式Whole-Proof 模式比如早期的 DeepSeek-Math-V2 或 AlphaProof 的部分变体要求模型一次性生成几千行 Lean 代码然后交给 Lean 编译器“一锤定音”。这就像让一个刚学微积分的学生直接闭卷默写《Principia Mathematica》全书。它的致命缺陷不是能力不足而是反馈粒度太粗、纠错成本太高。一次编译失败错误信息可能是invalid occurrence of x也可能是failed to synthesize instance甚至只是某个import语句漏了分号。模型无法区分这是语法错误、类型错误还是逻辑断层。更关键的是它无法复用中间成果——哪怕前 99 行完全正确只要第 100 行错了整个证明就作废所有 token 都成了沉没成本。Seed Prover 1.5 的 Agentic 架构其第一刀就砍向了这个模式。它强制模型以“lemma”引理为最小单元进行交互。每一轮模型只生成一个独立、可验证的引理例如lemma my_lemma : ∀ a b : ℝ, a b b a : by ring。这个引理被送入 Lean 验证器返回的结果只有两种success或failure且 failure 附带精确到行号和错误类型的结构化反馈。这种设计带来的根本性变化是模型的学习目标从“生成正确代码”变成了“做出正确决策”。它不再需要背下所有 mathlib 定理的完整签名而是需要判断此刻我该调用mathlib search找一个加法交换律的已有定理还是该调用python exec先算几个数值例子验证猜想这个决策过程就是 Agentic 的灵魂。2.2 “工具集成”不是功能列表而是构建了一个可编程的推理环境很多介绍会把 Seed Prover 1.5 的工具列成三点Lean 验证、Mathlib 搜索、Python 执行。但这严重低估了其设计深度。这三者不是并列的插件而是一个有严格依赖关系和状态流转的推理环境Reasoning Environment。Lean 验证器LooKeng是这个环境的“心脏”和“裁判”。它不是一个简单的lean --run命令封装而是一个基于 Python 的 REPL4 接口。这意味着模型与 Lean 的每一次交互都发生在同一个持久化的运行上下文中。上一轮成功证明的lemma A会被自动缓存到内存中并成为下一轮推理的“已知事实”。这直接解决了 Whole-Proof 模式最大的上下文浪费问题。实测下来一个中等难度的 Putnam 题Whole-Proof 模式可能需要 40K tokens 来重复携带所有前置引理而 Agentic 模式通过增量缓存将有效上下文压缩到 15K tokens 以内效率提升近三倍。Mathlib 搜索器是这个环境的“图书馆管理员”。它不是简单地对 mathlib 文档做全文检索而是使用 embedding-based retrieval嵌入式检索将用户查询如 “how to prove inequality with squares”映射到语义空间再从固定 commitv4.22.0的 mathlib4 代码库中召回最相关的定理、引理或定义。关键在于“固定 commit”——这保证了结果的可重现性。你在周一跑出的搜索结果和我在周三跑出的必须完全一致。否则模型学到的“调用搜索器的策略”就会失效。Seed Prover 1.5 的论文里提到Fate-H 问题平均需要 10 次搜索而 Putnam 只需 1-2 次这背后反映的正是不同难度问题对 mathlib 知识依赖程度的差异。模型不是在盲目搜索而是在学习“什么问题该搜什么问题该自己推”。Python 执行器是这个环境的“实验台”。它允许模型生成并运行任意 Python 代码用于数值验证、符号计算、甚至生成反例。例如面对一个关于数列极限的猜想模型可以先生成import sympy as sp; n sp.symbols(n); limit_expr ...; print(sp.limit(limit_expr, n, sp.oo))拿到一个数值结果后再决定下一步是尝试induction还是squeeze_theorem。这个设计的精妙之处在于它把“计算实验”这个人类数学家最常用的直觉工具正式纳入了形式化推理的闭环。它不再是模型“脑内模拟”而是真刀真枪地跑出来看结果。我试过一个案例一个涉及高次多项式根的 Putnam 题模型在第一次尝试apply polynomial_root_theorem失败后立刻调用 Python 计算判别式发现其为负从而转向complex_conjugate_roots的思路。这个决策链条是纯语言模型永远无法自发形成的。提示Agentic 架构的“智能”80% 体现在工具调用的时机和组合上而非单次生成的文本质量。一个优秀的 Agentic Prover应该像一个经验丰富的数学系助教他不一定能立刻写出最优雅的证明但他知道什么时候该查教材Mathlib Search什么时候该拿计算器按几下Python Exec什么时候该把问题拆成小块Lemma Generation什么时候该回头重读题干Self-Summarization。2.3 Sketch Model不是翻译器而是“自然语言与形式语言之间的战略指挥官”Sketch Model 常被误解为一个 NL2Lean 的翻译模型。这是巨大的偏差。它的核心任务是战略分解Strategic Decomposition。给定一个自然语言证明草稿例如“由均值不等式我们有 A ≥ B再由柯西不等式B ≥ C故 A ≥ C”Sketch Model 的工作不是逐字翻译而是识别出其中隐藏的、可独立验证的“战术支点”Tactical Anchors并将其转化为一组带有占位符sorry的 Lean 引理。例如它会生成lemma part1 : A ≥ B : sorry lemma part2 : B ≥ C : sorry theorem main : A ≥ C : calc A ≥ B : part1 ... ≥ C : part2这个过程的价值在于它把一个单点突破的难题转化为了一个可并行、可调度、可容错的多任务问题。Agentic Lean Prover 可以同时启动三个子进程分别去攻克part1、part2和main。如果part1在 5 分钟内无解系统不会放弃整个证明而是可以触发“递归分解”让 Sketch Model 基于part1的失败生成更细粒度的子引理part1a,part1b…… 这种“证明树Proof Tree”的动态生长能力是 Whole-Proof 模式完全不具备的。Sketch Model 的训练也印证了这一点它的奖励函数R 1仅当N_lemmas ≥ 3 AND S_FL ≥ 0 AND S_NL ≥ 0.7。它不鼓励生成一个完美的大引理而是奖励生成至少三个、结构正确、语义合理的子引理。这从根本上扭转了模型的优化方向——从追求“单次成功率”转向追求“分解有效性”。3. 实操细节解析从零开始搭建一个可调试的 Seed Prover 1.5 环境3.1 环境准备VS Code Python Lean4 的黄金三角Seed Prover 1.5 的实操门槛远低于你的想象。它不依赖昂贵的 TPU 集群一个配置合理的个人工作站即可完成大部分调试工作。核心是搭好“VS Code Python Lean4”这个黄金三角。Python 环境必须使用Python 3.10 或 3.11。这是 LooKengLean 验证接口和 mathlib4 的硬性要求。我强烈建议使用pyenv进行版本管理避免与系统 Python 冲突。安装命令pyenv install 3.11.9 pyenv global 3.11.9 pip install --upgrade pip setuptools wheel注意不要用 Anaconda虽然它方便但其内置的pip和conda通道经常导致lean和mathlib4的依赖冲突。我踩过坑conda install lean会强行降级你的 Python 版本导致后续所有步骤失败。Lean4 安装官方推荐使用elanLean Installer。这是最稳定的方式。# 下载并安装 elan curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh # 重启终端然后安装 Lean4 最新稳定版 elan default stable # 验证安装 lean --version # 应输出类似 Lean (version 4.8.0, commit ...VS Code 配置这是最关键的一步。你需要三个核心插件Lean4官方插件提供语法高亮、实时错误检查、#check命令支持。PythonMicrosoft 官方插件用于编辑和运行 Python 脚本。Remote - SSH可选但强烈推荐如果你的主力开发机是 Mac/Windows而 Lean 环境部署在 Linux 服务器上SSH 插件能让你无缝连接享受本地编辑、远程执行的体验。配置settings.json的关键项{ python.defaultInterpreterPath: /Users/yourname/.pyenv/versions/3.11.9/bin/python, lean4.leanPath: /Users/yourname/.elan/toolchains/leanprover--lean4---stable/bin/lean, lean4.leanpkgPath: /Users/yourname/.elan/toolchains/leanprover--lean4---stable/bin/leanpkg }这些路径必须与你实际的pyenv和elan安装路径完全一致。一个字符的错误都会导致 VS Code 无法识别 Lean 文件。3.2 Mathlib4 的“精准锚定”为什么 commit ID 比版本号更重要Seed Prover 1.5 的论文明确指出其 Mathlib 搜索器“calibrated to a fixed Mathlib commit (i.e., v4.22.04.22.0)”。这个v4.22.04.22.0不是一个版本号而是一个 Git commit hash 的别名。它指向 mathlib4 仓库在 2024 年 4 月 22 日的一个特定快照。这是确保结果可重现的基石。安装指定 commit 的 mathlib4不能用leanpkg upgrade而必须手动克隆# 创建一个干净的工作目录 mkdir seed-prover-demo cd seed-prover-demo # 初始化 lean 项目 leanpkg init my_project # 进入项目目录删除默认的 mathlib 依赖 rm -rf .lake/packages/mathlib4 # 手动克隆指定 commit 的 mathlib4 git clone https://github.com/leanprover-community/mathlib4.git .lake/packages/mathlib4 cd .lake/packages/mathlib4 git checkout v4.22.04.22.0 cd ../.. # 更新 lakefile.lean确保它引用了正确的 mathlib4 路径 # 通常 lakefile.lean 会自动生成无需手动修改完成这一步后在 VS Code 中打开一个.lean文件你会看到左下角状态栏显示mathlib4 (v4.22.04.22.0)。这才是一个可信赖的、与 Seed Prover 1.5 论文结果对齐的环境。任何其他 commit都可能导致mathlib search返回完全不同的结果进而让模型的“搜索策略”失效。3.3 LooKeng 接口如何让 Python 与 Lean 进行“心跳式”通信LooKeng 是 Seed Prover 1.5 的“神经系统”。它不是一个黑盒 API而是一个你可以随时查看、修改、调试的 Python 模块。其核心逻辑非常清晰# pseudo-code for LooKengs core loop def run_lean_code(lean_code: str, context: LeanContext) - LeanResult: context: 包含所有已缓存 lemma 的运行时上下文 LeanResult: 结构化对象包含 success: bool, error_line: int, error_msg: str, new_context: LeanContext # 1. 将 lean_code 和 context 中的所有已缓存 lemma 拼接成一个完整的 Lean 文件 full_code \n.join(context.cached_lemmas) \n lean_code # 2. 启动一个临时的 Lean 进程传入 full_code result subprocess.run( [lean, --run, -], inputfull_code, textTrue, capture_outputTrue, timeout30 # 关键必须设置超时防止 Lean 卡死 ) # 3. 解析 Lean 的 stdout/stderr提取结构化信息 return parse_lean_output(result.stdout, result.stderr)要真正掌握 Seed Prover 1.5你必须亲手写一个最简版的 LooKeng 调用脚本。创建一个test_looken.pyfrom looken import LooKeng # 假设你已安装或克隆了 looken 模块 # 初始化一个空的 Lean 上下文 lk LooKeng() # 尝试证明一个最简单的引理 code lemma test_add : 1 1 2 : by rfl result lk.run(code) print(fSuccess: {result.success}) if not result.success: print(fError at line {result.error_line}: {result.error_msg}) else: print(Proof cached!) # 查看当前上下文缓存了什么 print(fCached lemmas: {list(lk.context.cached_lemmas.keys())})运行这个脚本你会第一次直观地看到 Agentic 架构的“心跳”一次成功的rfl调用不仅返回了successTrue还把test_add这个引理的名字存进了context。这就是增量式推理的起点。没有这一步后续所有的“缓存复用”、“状态流转”都无从谈起。3.4 工具调用的“原子性”与“组合性”如何设计一个鲁棒的 Tool Call SchemaSeed Prover 1.5 的提示词Prompt中工具调用被设计为具有严格 Schema 的 JSON 对象。这不是为了炫技而是为了工程上的鲁棒性。一个典型的工具调用长这样{ tool: mathlib_search, query: commutativity of addition for real numbers, max_results: 3 }而 Python 执行器的调用则是{ tool: python_exec, code: print(2**10) }关键在于模型的输出必须被严格解析为这种格式。任何语法错误比如少了一个逗号或者query字段用了中文引号都会导致整个工具调用失败进而中断推理链。因此在实操中你必须为你的模型输出添加一层“Schema Guard”import json import re def parse_tool_call(model_output: str) - dict: 从模型输出中提取并解析 tool call JSON # 使用正则安全地提取 JSON 块避免被模型输出的其他文本干扰 json_match re.search(r\{.*?\}, model_output, re.DOTALL) if not json_match: raise ValueError(No JSON object found in model output) try: tool_call json.loads(json_match.group()) # 验证必需字段 if tool not in tool_call: raise ValueError(Missing tool field) if tool_call[tool] not in [mathlib_search, python_exec, lean_verify]: raise ValueError(fUnknown tool: {tool_call[tool]}) return tool_call except json.JSONDecodeError as e: raise ValueError(fInvalid JSON: {e}) # 在你的主循环中使用 model_output llm.generate(prompt) try: tool_call parse_tool_call(model_output) result execute_tool(tool_call) # 你的工具执行函数 except ValueError as e: # 捕获所有解析错误记录日志并触发 fallback 策略如让模型重试 log_error(fTool call parsing failed: {e}) prompt f\nERROR: {e}. Please output a valid JSON tool call.这个parse_tool_call函数就是你实操环境的“安全阀”。它确保了无论模型多么“调皮”你的系统都不会因为一个格式错误而崩溃。这是我从生产环境中总结出的最重要的一条经验Agentic 系统的稳定性不取决于模型的上限而取决于你为它设置的下限。4. 核心环节实现手把手复现一个 Putnam 题目的完整推理轨迹4.1 题目选择与预处理为什么 Putnam 2025 A1 是最佳入门题Putnam 2025 A1 题目是“Let $f(x)$ be a continuous function on $[0,1]$ such that $\int_0^1 f(x) dx 0$. Prove that there exists $c \in (0,1)$ such that $f(c) 0$.” 这是一个经典的介值定理Intermediate Value Theorem应用题。它之所以是绝佳的入门题原因有三知识边界清晰它只依赖continuous、integral、IVT这几个核心概念全部在 mathlib4 的基础库中无需复杂的高级分析。证明路径唯一标准解法就是构造辅助函数 $F(x) \int_0^x f(t) dt$利用 $F(0)F(1)0$ 和罗尔定理Rolles Theorem再结合 $F(x)f(x)$。这条路径非常线性便于你追踪模型的每一步决策。失败点明确最常见的失败是模型忘记声明f是连续的或者在调用rolle时未能正确提供differentiable_on的前提。这些失败点正是你理解 Agentic 架构“反馈驱动”特性的最佳教材。在 VS Code 中新建一个putnam_a1.lean文件写入题目声明import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.Integration.IntegrableOn import Mathlib.Analysis.SpecialFunctions.Pow.Real open Real -- Putnam 2025 A1 theorem putnam_a1 (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_int : ∫ (x : ℝ) in Set.Icc 0 1, f x 0) : ∃ c ∈ Set.Ioo 0 1, f c 0 : by -- 我们将在这里引导模型一步步完成证明4.2 第一阶段Sketch Model 的战略分解现在我们模拟 Sketch Model 的工作。给定这个 Lean 陈述它会生成一个引理式的 Sketch。一个高质量的 Sketch 应该是-- Sketch generated by Sketch Model lemma putnam_a1_aux1 (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_int : ∫ (x : ℝ) in Set.Icc 0 1, f x 0) : ∃ c ∈ Set.Ioo 0 1, f c 0 : by -- Step 1: Define the auxiliary function F(x) ∫₀ˣ f(t) dt let F : ℝ → ℝ : fun x ∫ (t : ℝ) in Set.Icc 0 x, f t -- Step 2: Prove F is differentiable and F f have hF_diff : DifferentiableOn ℝ F (Set.Icc 0 1) : sorry have hF_deriv : ∀ x ∈ Set.Icc 0 1, deriv F x f x : sorry -- Step 3: Prove F(0) 0 and F(1) 0 have hF0 : F 0 0 : sorry have hF1 : F 1 0 : sorry -- Step 4: Apply Rolles theorem to F on [0,1] have hRolle : ∃ c ∈ Set.Ioo 0 1, deriv F c 0 : sorry -- Step 5: Conclude f(c) 0 exact hRolle.trans (fun c hc hF_deriv c hc)注意所有sorry都是占位符。Sketch Model 的任务到此为止。它成功地将一个“存在性证明”分解为了 5 个逻辑上环环相扣、且每个都比原命题更易处理的子目标。这 5 个sorry就是 Agentic Lean Prover 的 5 个待办任务To-Do Items。4.3 第二阶段Agentic Prover 的工具驱动式求解现在Agentic Prover 开始工作。它会针对hF0 : F 0 0这个子目标发起第一轮交互。Prompt 输入模型看到的是F 0 0的目标以及当前上下文包含了F的定义和hf_int的假设。模型决策它意识到F 0的定义是∫₀⁰ f(t) dt根据积分的基本性质这个值恒为 0。但它不确定 mathlib 中对应的定理名称。工具调用于是它发出第一个mathlib_search请求{tool: mathlib_search, query: integral from a to a is zero, max_results: 1}LooKeng 执行LooKeng 调用 embedding 检索返回最相关的结果integral_Icc_self其声明为∀ {α : Type*} [NormedAddCommGroup α] [MeasurableSpace α] [IsCompleteSpace α] [HasIntegral α] (a : α), ∫ (x : α) in Set.Icc a a, f x 0。模型响应模型收到结果后生成 Lean 代码have hF0 : F 0 0 : integral_Icc_self 0并将其提交给 LooKeng 验证。LooKeng 将hF0的定义与上下文拼接运行 Lean返回success。hF0被加入缓存。接下来模型处理hF1 : F 1 0。它再次调用mathlib_search但这次查询integral from 0 to 1 equals given value得到integral_eq_zero_of_integral_eq_zero。它意识到hf_int直接给出了∫₀¹ f 0所以hF1就是hf_int本身。它生成have hF1 : F 1 0 : hf_int验证通过。这个过程的关键在于模型不是在“猜”定理而是在“查”定理。它的知识库是 mathlib4 的完整代码它的“记忆”是当前上下文的缓存。每一次mathlib_search都是对这个庞大知识库的一次精准定位。而hF0和hF1的成功为后续调用rolle提供了坚实的基石。4.4 第三阶段失败、回溯与自我总结Self-Summarization最难的部分是hF_diff和hF_deriv。模型可能会尝试直接调用fundamental_theorem_of_calculus但发现其前提条件过于复杂需要f是 Riemann integrable而hf_cont只保证了连续性。它会失败几次。这时Agentic 架构的“自适应”特性就显现了。系统会触发Self-Summarization。模型会收到一个新 PromptYou have failed to prove hF_diff and hF_deriv. Summarize what you know so far: - F is defined as the integral of f. - f is continuous on [0,1]. - You need to show F is differentiable and its derivative is f. What theorem in mathlib connects continuity of f to differentiability of its integral?模型会生成一个摘要例如“We know f is continuous. By the Fundamental Theorem of Calculus, Part I, if f is continuous on [a,b], then the function F(x) ∫ₐˣ f(t) dt is differentiable on (a,b) and F(x) f(x). We need to find the mathlib theorem for FTC-I.”这个摘要就是一次“元认知”Metacognition的体现。模型不再执着于失败的路径而是退后一步重新审视问题的核心约束f连续和目标F可导并据此生成一个更精准的mathlib_search查询。最终它会找到continuous_on.integral_hasDerivAt并成功完成证明。实操心得Self-Summarization 不是“重来一遍”而是“带着地图重走一遍”。它把失败的经验编码成了下一次搜索的元信息。这是 Agentic 系统区别于传统 LLM 的核心进化。5. 常见问题与排查技巧实录一份来自真实调试现场的速查表问题现象根本原因排查步骤解决方案我的实操心得LooKeng 报错timeout或subprocess.CalledProcessErrorLean 进程卡死通常是由于rfl或simp在一个无限循环中耗尽了资源。1. 检查run_lean_code函数中的timeout参数是否过小建议初始设为 60 秒。2. 在 VS Code 中手动打开一个.lean文件粘贴相同的代码看 Lean Server 是否也卡住。在 Lean 代码中显式添加set_option maxHeartbeats 0和set_option maxRecDepth 1000禁用 Lean 的内部超时让 LooKeng 的超时成为唯一控制点。Lean 的默认超时机制和 Python 的subprocess超时机制是两套独立的系统必须统一由 Python 层控制否则会出现“Python 已杀进程但 Lean 进程还在后台跑”的诡异状态。mathlib_search返回空结果或无关结果1. 当前 mathlib4 commit 不匹配。2. 查询语句query语义模糊embedding 检索效果差。1. 运行cd .lake/packages/mathlib4 git log -n 1确认 commit hash 是v4.22.04.22.0。2. 在 VS Code 中用 Lean4 插件的#search命令手动输入相同 query看结果是否一致。1. 严格校验 commit。2. 将 query 改为更具体的 mathlib 定理名的一部分例如不搜 “derivative of integral”而搜 “hasDerivAt_integral”不搜 “intermediate value”而搜 “intermediate_value_theorem”。Mathlib 的 embedding 检索对“定理名关键词”的敏感度远高于对“自然语言描述”的敏感度。把它当成一个增强版的grep而不是一个语义搜索引擎。模型反复生成语法错误的 Lean 代码如:后面少了by模型的训练数据中Lean 语法的 token 分布不均衡导致它对某些语法结构的“概率”估计不准。1. 检查模型输出的原始字符串确认错误是语法错误syntax error还是逻辑错误tactic failed。2. 查看 LooKeng 的error_msg确认错误类型。在parse_tool_call之后添加一个syntax_guard步骤用 Lean 的Parser模块import Lean.Parser对生成的 Lean 代码进行预解析。如果预解析失败立即拒绝该输出并提示模型“Your Lean code has syntax errors. Please check the grammar and retry.”语法错误是最低级的错误但也是最致命的。因为它会污染整个上下文。宁可多花 100ms 做一次预解析也不要让一个语法错误的lemma进入缓存导致后续所有推理都建立在沙堡之上。python_exec返回NameError或ModuleNotFoundErrorPython 执行环境与你的开发环境隔离缺少必要的包。1. 在python_exec的实现中打印sys.path。2. 运行pip list确认sympy、numpy等常用包是否存在。在python_exec的code前自动注入import sys; sys.path.append(/path/to/your/libs)并将你常用的科学计算包sympy,numpy,scipy预先安装到该环境中。不要把python_exec当成一个玩具。它是你的“计算实验台”必须和你的主力 Python 环境保持一致。我专门为此建了一个prover-envconda 环境并在python_exec中硬编码了它的路径。整个推理链在Pass3 × 3后停止但问题未解决这是正常行为表示当前的 Sketch 分解策略或 Agentic Prover 的能力边界已达极限。1. 检查Pass3 × 3的具体含义3 次并行尝试每次最多 3 轮交互。2. 查看最后一次失败的error_msg判断是哪个子目标卡住了。触发“递归分解”将当前失败的sorry作为新的theorem重新喂给 Sketch Model生成一个更细粒度的 Sketch。例如将hF_diff分解为hF_cont证明 F 连续和hF_diff_from_cont从连续性推出可导性。“失败”不是终点而是下一次分解的起点。Agentic 架构的威力不在于它永不失败而在于它能把每一次失败都转化为一次更精细的、更有希望的成功。6. 经验总结与延伸思考Agentic 架构的普适性启示Seed Prover 1.5 的价值早已超越了数学定理证明本身。它提供了一种通用的、可迁移的“复杂任务求解范式”。我最近就在一个完全不相关的项目中复用了它的核心思想一个自动化生成合规性审计报告的系统。我们把“审计标准”当作mathlib把“企业提供的原始数据”当作natural language proof把“审计规则引擎”当作Lean verifier把“SQL 查询生成器”当作python_exec。整个系统的架构图和 Seed Prover 1.5 的 Figure 2 几乎一模一样。这印证了一个深刻的道理**Agentic 架构的本质是将一个不可控的、端到端的“黑箱生成”问题拆解为一个可控