Leanstral 1.5 能写策略、Lean 编译器说了算

Leanstral 1.5 能写出看起来像样的 tactic，但它给出的只是候选，不是已经成立的证明。真正说了算的是 Lean 编译器：一条策略能不能留下来，取决于 lake build 能不能在没有 sorry 的情况下通过。可行的做法是把流程拆成生成候选、逐条编译、只合并通过项三步，模型负责发散，编译器负责收敛。

适用场景：Lean 4 项目里有 sorry 待补全的小引理。操作动作：用信息面板或 #check 抄下目标与假设，让模型按可能性排序返回多条 tactic，逐条替换 sorry 跑编译，只留编译器接受的。验证方式：全量 lake build 无报错、无残留 sorry。风险边界：编译通过只说明类型成立，不代表思路最优；模型对引理名可能记错，版本差异需自行确认。

在 Lean 文件里标出需要策略补全的证明状态

先把模型要解决的问题固定下来。在 Lean 4 编辑器扩展里，把光标停在 sorry 上，信息面板会显示当前目标与上下文假设；没有面板时，可以在同一位置临时加 #check 或 #print 确认名字是否存在。这两处输出就是喂给模型的原文，不要改写成自然语言，因为 +、⊢、命名空间这些符号一旦转述就容易失真。

-- Foo.lean
theorem add_zero_right (n : Nat) : n + 0 = n := by
  sorry

信息面板对应输出通常长这样：

n : Nat
⊢ n + 0 = n

把它整理成两段文本片段：一段写假设，每行是 名字 : 类型；一段写目标，以 ⊢ 开头；再附上你确认过存在的引理名，例如 Nat.add_zero。引理名要靠 #check @Nat.add_zero 这类命令验证，不要凭记忆写进提示词。

让 Leanstral 1.5 生成候选 tactic 列表

一次要多个候选，比一轮一轮追问更省事，也方便后面按编译结果筛选。提示词的关键约束是：按可能性排序、每行一条、不附加解释。解释会占掉输出长度，而且对编译结果没有影响。

你是一名 Lean 4 策略助手。下面是一个待补全的证明状态。

假设：
n : Nat

目标：
⊢ n + 0 = n

已确认可用的引理：Nat.add_zero

请给出可以替换 sorry 的 tactic 候选，按最可能成功的顺序排列。
要求：
1. 每行只写一条候选，直接写 by 块内的单行内容；
2. 不要编号，不要解释，不要代码围栏；
3. 最多 8 行；
4. 只使用 Lean 核心库或 Mathlib 中确实存在的名字，不确定就不要写。

如果目标里有多个假设或前后依赖，把假设原样贴全，并注明是否允许使用 Mathlib。返回结果先当草稿看，不要直接粘进文件就提交。

逐条粘贴候选并运行 Lean 编译

把候选一条一条替换掉 sorry，每次只放一条，编译完记下结果再换下一条。单文件快速检查用 lake env lean，最终判断仍以整工程构建为准。

cd your-lean-project

# 单文件检查，快一些
lake env lean Foo.lean

# 整工程构建，最终依据
lake build

把每条策略和编译输出对应记下来，形式随手就行：

exact Nat.add_zero n      -> ok
simp                      -> ok
rw [Nat.add_zero]         -> ok
omega                     -> ok
linarith                  -> error: tactic failed
exact Nat.add_zero_comm   -> error: unknown identifier

这里要提醒一点：lake env lean 只编译你指定的文件，能过不代表工程里其他地方也没问题；合并阶段的判断必须回到 lake build。

把编译失败的策略和错误信息归类

失败信息不用逐条细读，先归成三类就能判断下一步动作。

unknown identifier：模型写了一个不存在的引理名，或者命名空间没打开。例：目标是 n + 0 = n，候选写 exact Nat.add_zero_comm n，编译器报 unknown identifier 'Nat.add_zero_comm'。处理方式是先用 #check 找真实名字，再确认是否需要 open Nat。
type mismatch：引理存在，但类型或方向对不上。例：候选写 exact Nat.zero_add n，它给出的类型是 0 + n = n，与目标 n + 0 = n 不匹配。处理方式是 #check @Nat.zero_add 看清签名，调整参数或换成方向正确的引理。
tactic failed：策略本身有效，但它解决不了这个目标。例：在只有 n : Nat 的目标上直接上 linarith，报 tactic failed。处理方式是先化简目标，例如 simp only [...] 或 norm_num，或者换成对该目标更合适的策略如 omega。

另外 unsolved goals 通常意味着策略只走了一步、目标还在，这类候选择可以保留思路但要补后续步骤。归类的作用是决定该重写候选还是换策略，而不是让你一条条去猜。

只把编译通过的策略合并进证明脚本

通过编译的候选可能有好几条，选哪条要看长期可维护性。通常优先选最短、依赖最少的那条：exact、rfl 这类只依赖明确引理的写法，比大范围 simp 更稳，因为 simp 的默认集合会随库版本变化，今天能过不代表下次构建还能过。如果只能靠 simp，可以先用 simp only [Nat.add_zero] 把范围收窄。

合并前做清理：删掉测试时留下的注释、临时的 #check 行、为试验加的 import 和 set_option。然后重新跑一次完整构建，并确认没有残留的占位证明：

grep -rn "sorry" `--include`=*.lean .

lake build

最终标准只有两条：lake build 无错误，grep 找不到 sorry。达到这两条，模型写的策略才算真正进了证明脚本；达不到就退回候选列表重新筛选，不要用注释或临时引理绕过去。