23.2.1. 工作流程🔗

❶ Lean 把问题编码为外部格式（DIMACS、SMT-LIB、JSON）
❷ 启动外部进程，发送问题
❸ 外部工具求解，返回证书（resolution proof、多项式系数等）
❹ Lean 解析证书，在内核中验证正确性
❺ 验证通过 → 构造 Lean 证明项

安全性：即使外部工具有 bug 或返回垃圾数据， Lean 内核会拒绝不正确的证书。外部工具不在可信基础（TCB）中。

23.2.2. 案例：polyrith🔗

-- [示意] polyrith 的使用
example (a b : ℚ) (h1 : a + b = 3) (h2 : a - b = 1) :
    a = 2 := by
  polyrith
  -- ▸ 内部流程：
  -- ❶ 编码：把 h1、h2 和目标转为多项式约束，序列化为 JSON
  -- ❷ 调用：发送给 Sage 服务器（远程 HTTP 请求）
  -- ❸ 求解：Sage 计算 Gröbner 基，找到系数 1/2 * h1 + 1/2 * h2
  -- ❹ 返回：系数作为证书
  -- ❺ 验证：Lean 用系数构造 linear_combination，由 ring 验证

关键：Sage 不在 TCB 中——验证完全由 ring 在 Lean 内核完成。

23.2.3. 案例：SAT 证书🔗

❶ Lean 把命题编码为 CNF（DIMACS 格式）
❷ 调用 CaDiCaL
❸ 求解器返回 LRAT 证书（resolution proof 的紧凑表示）
❹ Lean 中的 LRAT checker 验证每一步 resolution

LRAT 是 SAT 竞赛标准——Lean 只需一个高效 LRAT checker 即可对接任意求解器。

23.2.4. 证书模式的代价🔗

• 编码/解析开销：MetaM 端代码量不小

• 验证开销：内核验证证书消耗 heartbeats

• 证书膨胀：SAT 的 resolution proof 可达 GB 级

• 工具依赖：需要外部工具可用（网络或本地安装）

23.3.1. Oracle vs native_decide🔗

• 逻辑层面 —— native_decide：不引入新公理 —— Oracle（sorry/自定义公理）：引入不可验证的假设

• 可信基础 —— native_decide：Lean 内核 + 编译器 —— Oracle（sorry/自定义公理）：Lean + 外部工具

• 失败时 —— native_decide：类型错误 —— Oracle（sorry/自定义公理）：可能引入矛盾

• Mathlib —— native_decide：谨慎使用 —— Oracle（sorry/自定义公理）：不接受

native_decide 不是 oracle——它在已信任的编译环境中做更快的判定计算。

23.3.2. Oracle 的合理场景🔗

❶ 快速原型：用 sorry 标记子目标，先完成整体架构
❷ 开发迭代：信任外部结果以加速编辑-编译循环
❸ 最终替换：逐步把 sorry 替换为证书模式或手动证明

永远不要把含 sorry 的代码合并到主分支。 #check_no_sorry 和 Mathlib CI 强制执行这一纪律。

23.4.1. IO.Process.spawn——流式交互🔗

-- [示意] 启动外部进程并流式通信
def callSolver (problem : String) : IO String := do
  let child ← IO.Process.spawn {
    cmd := "z3"                    -- ❶ 可执行文件
    args := #["-in", "-smt2"]     -- ❷ 命令行参数
    stdin := .piped                -- ❸ 管道式 stdin/stdout
    stdout := .piped
    stderr := .piped
  }
  child.stdin.putStr problem       -- ❹ 写入问题
  child.stdin.flush
  let stdout ← child.stdout.readToEnd  -- ❺ 读取输出
  let exitCode ← child.wait
  if exitCode ≠ 0 then
    throw <| IO.userError s!"z3 failed with exit code {exitCode}"
  return stdout

23.4.2. IO.Process.output——一次性调用🔗

-- [示意] 简便版本，适合短时脚本
def callScript (input : String) : IO String := do
  let result ← IO.Process.output {
    cmd := "python3"
    args := #["solver_script.py", "--input", input]
  }
  -- ▸ result : { exitCode : UInt32, stdout : String, stderr : String }
  if result.exitCode ≠ 0 then
    throw <| IO.userError s!"script failed: {result.stderr}"
  return result.stdout

23.4.3. 在 tactic 中使用🔗

TacticM → MetaM → 可执行 IO：

-- [示意] 在 tactic 中调用外部工具
elab "external_solve" : tactic => do
  let goal ← getMainTarget
  let smt2 := encodeGoal goal          -- ❶ 编码
  let result ← callSolver smt2         -- ❷ 调用（IO 操作）
  match parseSolverOutput result with   -- ❸ 解析
- .sat cert =>
    let proof ← verifyCertificate cert goal  -- ❹ 验证证书
    closeMainGoal proof
- .unsat   => throwError "solver says unsat"：.unknown => throwError "solver returned unknown"

23.6.1. 架构🔗

  Lean Server ──→ LLM API ──→ tactic 候选 ["simp", "ring", ...]
  (目标 + 上下文)                       │
       └── 逐个尝试执行 ←──────────────┘
           验证通过 → 接受；全部失败 → 报错

23.6.2. 实现骨架🔗

-- [示意]
elab "llm_suggest" : tactic => do
  let goal ← getMainTarget
  let ctx ← getLocalHypotheses
  let response ← callLLM (formatPrompt goal ctx)  -- ❶ 调用 LLM
  let candidates ← parseTactics response           -- ❷ 解析候选
  for tac in candidates do                          -- ❸ 逐个尝试
    try
      evalTacticStr tac    -- 在 MetaM 中执行
      return               -- 成功 → 结束
    catch _ => continue
  throwError "all LLM suggestions failed"

23.6.3. 信任模型与防护🔗

LLM 不在 TCB 中——和 SAT 求解器地位相同：提供候选，Lean 内核裁决。

LLM 可能生成：             应对：
  正确 tactic             → 内核验证通过 ✓
  错误 tactic             → 内核拒绝 ✓
  包含 sorry 的 tactic     → 框架层面过滤 ⚠️

防护措施：过滤 sorry、每个候选设 heartbeat 上限、执行后检查目标是否全部关闭。

23.8.1. 可用性与 fallback🔗

polyrith 需要网络 → 失败时打印系数，用户手动写 linear_combination
SAT tactic 需本地安装 → 提供安装指引或 Docker 镜像
LLM tactic 需 API key → 优雅降级，给出清晰错误

23.8.2. 可复现性🔗

外部工具引入不确定性。解决方案：

• 缓存证书：polyrith 支持 --only 模式使用缓存系数

• 固化 LLM 建议：成功的 tactic 替换为确定性版本

• CI 独立：不依赖外部服务，只用缓存结果

23.9.1. 失败 1：外部工具不可用🔗

-- [示意]
-- ✗ 用户没装 z3
-- 错误：z3: command not found
-- ✓ tactic 应捕获 IO 错误并给出安装提示
-- ✓ 提供不依赖外部工具的 fallback

23.9.2. 失败 2：编码不完整🔗

-- [示意]
-- ✗ 目标涉及自定义类型，编码函数不识别 → 求解器返回 unknown
-- ✓ 诊断：打印编码后的 SMT-LIB 查看遗漏
-- ✓ 修复：扩展编码函数，或先 unfold/simp 消除未识别构造

23.9.3. 失败 3：证书验证失败🔗

-- [示意]
-- ✗ 外部工具 bug 导致错误证书 → Lean 验证失败
-- ✓ 这正是证书模式的价值——错误被捕获，不引入矛盾
-- ✓ 更新工具版本或报告 bug

23.9.4. 失败 4：Oracle 引入矛盾🔗

-- [示意]
-- ✗ 自定义公理 axiom smt_says (p : Prop) : p → 可证明 False
-- ✓ 用 sorry 而非自定义公理——sorry 至少有编译器警告
-- ✓ oracle 公理永远不要进入生产代码

23.9.5. 失败 5：LLM 建议含 sorry🔗

-- [示意]
-- ✗ LLM 返回 "intro h; sorry" → 框架不过滤则证明不完整
-- ✓ 执行前过滤 sorry；执行后检查无剩余目标

23.9.6. 失败 6：证书膨胀导致验证超时🔗

-- [示意]
-- ✗ 10 万变量 SAT 问题，resolution proof 100 万步 → heartbeats 爆炸
-- ✓ 用 native_decide 验证证书（而非内核归约）
-- ✓ 使用更紧凑的证书格式

23.11.1. 练习 1（设计）：选择集成模式🔗

对以下场景，选择证书模式、oracle 模式或 LLM 辅助，说明理由：

(a) Mathlib PR 中需要证明一个 200 变量的 SAT 问题。
(b) 个人项目探索阶段，需快速验证一批代数恒等式。
(c) 教学工具：学生输入定理，系统尝试自动找到证明。

提示：(a) 必须证书模式——Mathlib 不接受 sorry； (b) oracle（sorry）加速迭代，后续替换； (c) LLM 辅助——不确定性可接受，内核保证正确性。

23.11.2. 练习 2（分析）：可信基础对比🔗

列出以下证明方式的 TCB，从小到大排序：

(a) by ring
(b) by native_decide
(c) by polyrith（调用 Sage 后用 ring 验证）
(d) by sorry（信任外部 SMT 的口头声明）

提示：(a) Lean 内核；(b) 内核 + 编译器； (c) 和 (a) 相同（Sage 不在 TCB 中——证书由 ring 验证）； (d) 内核 + 外部 SMT + 人工判断。

23.11.3. 练习 3（进阶）：设计编码函数签名🔗

为以下场景设计类型签名（不需实现）：

-- (a) 把 Prop 目标编码为 SMT-LIB，需要返回变量映射以便解码
-- def encodeGoalToSMT : ??? := ...

-- (b) 解析 LRAT 证书
-- def parseLRAT : ??? := ...

提示： (a) Expr → MetaM (String × HashMap Expr String) (b) String → MetaM (List LRATStep)