用 Leanstral 1.5 补 Lean 证明步骤，跑一遍 Lean 4 编译器看是否通过

把 Leanstral 1.5 当成“候选策略生成器”，而不是“证明正确性的判定者”，是这个问题相对稳妥的用法：模型负责给出 by 之后可能成立的策略行，最终是否可用只由 Lean 4 编译器决定。判断路径很短——先在一个能编译的 Lean 项目里定位卡住的证明目标，把目标类型与假设整理成提示词，取回策略片段粘回 .lean 文件，运行 lake build 或 lake env lean，通过就留、不通过就把报错信息带回下一轮。没有 lake build 通过这一步，模型输出最多算草稿。

模型补的证明步骤看着合理但不确定能否进项目时，用 Lean 编译器做唯一验收标准：在可编译的项目里选一个 sorry 目标，记录目标类型与假设，让 Leanstral 1.5 只输出策略行，粘回原位置跑 lake build。通过则保留并提交；报错则把错误类型和原文追加进提示词重试，重试多次仍失败就换策略方向或手工补全。边界在于：未导入的引理、版本差异、simp 集合差异都可能导致模型输出失效，需要结合本地环境确认。

在 Lean 项目里定位卡住的证明目标

动手前先确认项目本身是干净的：在项目根目录跑一次 lake build，确保除了待补的 sorry 之外没有其他错误，否则后面无法区分是模型输出问题还是项目原有问题。然后找一个最小可复现的目标，例如下面这个文件，把 sorry 放在需要补全的位置：

-- Test/Append.lean
import Mathlib.Data.List.Basic

namespace Test

theorem mem_append_self (xs ys : List Nat) (h : 3 ∈ xs) : 3 ∈ xs ++ ys := by
  sorry

end Test

在 VS Code 装好 Lean 4 扩展后，把光标放在 sorry 上，右侧 Lean Infoview 会显示当前目标状态：假设栏里能看到 xs ys : List Nat 和 h : 3 ∈ xs，目标栏是 3 ∈ xs ++ ys。这份“假设 + 目标”就是后面提示词的核心内容，不要凭记忆手写，直接复制信息面板里的文本更可靠。如果目标里出现被折叠的定义（simp、omega 都不认识），可以临时加 set_option pp.all true 或 #check 辅助查看，但别把调试选项留在正式提交里。

让 Leanstral 1.5 生成候选策略或证明片段

提示词要约束两件事：只输出策略行，不改定理陈述；引理必须来自项目已导入的库。一个可复用的请求骨架如下，{BASE_URL}、{API_KEY}、{MODEL} 换成你所接入推理服务的实际地址、密钥和模型名，请求路径以该服务的实际文档为准：

POST {BASE_URL}/chat/completions
Authorization: Bearer {API_KEY}
Content-Type: application/json

{
  "model": "{MODEL}",
  "messages": [
    {"role": "user", "content": """
你是 Lean 4 证明助手。只为下面的证明目标补全策略，不要改动定理陈述，不要引入未声明的名字。

Lean 版本：4.x（以项目 lean-toolchain 为准）
已导入库：Mathlib.Data.List.Basic

假设：
xs ys : List Nat
h : 3 ∈ xs

目标：3 ∈ xs ++ ys

请输出：
1) 可直接放在 by 之后的策略代码，不含 theorem 行；
2) 每行策略的作用；
3) 用到的引理名，并说明是否在已导入库中。
"""}
  ]
}

如果项目没有用 Mathlib，提示词里的库要改成实际导入，否则模型倾向于给出 List.mem_append 这类不在当前环境里的名字，粘回去只会得到 unknown constant。返回值里若混入解释文字，可以要求“只给代码块”，或者自己剥出来——真正进文件的只有策略部分。

把候选片段粘贴进 .lean 文件并运行 lake build

把策略行替换掉 sorry，位置必须在 by 之后、缩进与原有策略一致：

theorem mem_append_self (xs ys : List Nat) (h : 3 ∈ xs) : 3 ∈ xs ++ ys := by
  exact List.mem_append.mpr (Or.inl h)

验证有两条粒度不同的命令：只想快速看单个文件，用 lake env lean Test/Append.lean，编译错误会直接打到终端；要确认整个项目没有连带问题，用 lake build。把输出重定向留档，方便下一轮把原文贴回提示词：

用 Leanstral 1.5 补 Lean 证明步骤，跑一遍 Lean 4 编译器看是否通过

lake build 2>&1 | tee build.log
# 或者只看单文件
lake env lean Test/Append.lean 2>&1 | tee lean-single.log

判定标准很简单：命令退出码为 0 且日志里没有 error，说明这条策略在该项目、该版本下成立，可以保留；出现 sorry 警告说明某个分支还没关闭，不算通过。注意 lake build 会缓存已编译模块，改完文件要确认日志里确实重新编译了目标文件，必要时先 lake clean 或删除对应 .olean。

根据编译器报错调整策略或让模型重试

报错信息本身是最好的下一轮输入。把错误类型、错误原文、目标状态一起追加进提示词，比笼统说“证明失败了”有效得多。下面两类最常见。

第一类是名字或策略不可用，例如 unknown constant 'List.mem_append_iff' 或 unknown tactic 'linarith'：前者通常是引理名记错或库没导入，后者是文件缺 import Mathlib.Tactic。追加提示词时可以写成“上一轮使用了 List.mem_append_iff，编译器报 unknown constant，请只使用 Mathlib.Data.List.Basic 中存在的引理，或改用 simp / exact 组合”。

第二类是类型不匹配或策略失败，例如 type mismatch, has type 3 ∈ xs but is expected to have type 3 ∈ xs ++ ys，或者 tactic 'omega' failed。这类说明方向对了但最后一步接错，提示词里补上“目标与假设的精确形式”和报错原文，要求模型给出更小步骤的分解，而不是一句 simp 或 omega 收尾。重试两三次仍不收敛，就回到手工补全，模型输出只作为思路参考。

记录哪些策略类型模型容易用错

把每次失败按策略类型归档，比记住具体某个定理更有价值。常见失败模式大致集中在几块：

归纳：模型常直接 induction xs 而不先 generalize 或 revert 依赖的假设，导致归纳假设里缺少需要的条件；有时还会写错构造子名（List.nil / List.cons 与实际归纳名不一致）。
重写：rw 方向错误（该用 ← h 写成了 h），或者重写的等式在目标中根本不存在，报 did not find instance of the pattern；含 ∈ 这类记号的等式更容易出问题。
算术：omega、linarith、nlinarith 缺少前提假设，或目标里出现整除、自然数减法、Int 与 Nat 混用，导致策略无能为力；模型还容易给出需要额外 Nat.sub 引理才能走通的写法。
自动化兜底：模型偏向用 simp、aesop 一句收尾，本地 simp 集合与模型假设不同，往往不通过，或者通过得很慢。

维护一个只保留编译通过策略的清单：每条记录写明目标形态、通过的策略、Lean 版本和导入库。没通过编译的片段不要写进清单，也不要直接进主干；可以放在本地草稿文件里，等确认后再合并。这样下次遇到同类目标，先查清单，再决定是否调用 Leanstral 1.5，比每次都从零试错稳一些。