模型给的证明总差一步，通常不是单一原因。一类是提示词没交代当前 Lean 版本、已导入的库和可用引理，模型只能按它记忆里的写法去补最后一步；另一类是本地 Lean 工具链版本与模型见过的写法不一致，同一个引理在不同版本里改名、换命名空间或被废弃。可操作的判断顺序是：先把问题塞进一个最小文件复现，再分别只动提示词、只动 Lean 版本各跑一次，最后用 #check 确认模型引用的引理在当前文件里是否真的可见。三类证据分开收集，才不至于把环境问题当成提示词问题反复调措辞。

如果证明每次只差最后一步，优先怀疑两件事：提示词里缺 Lean 版本与导入清单，或本地工具链版本与模型假设的版本不同。做法是固定最小 .lean 文件复现失败，再用同一提示词在两个 Lean 版本下各跑一次，并用 #check 验证引理可见性。证据不足时不要先换版本或大改提示词，版本切换会影响整条工具链，需要结合项目实际确认。

固定一个最小 Lean 文件复现差一步的证明

项目里文件多、import 多、命名空间层层嵌套时，很难判断模型缺的是哪一步。先建一个只含单个定理和 sorry 的文件，把“差一步”稳定复现出来，后面所有对比都基于它。建议放在一个干净的目录里，用 lake 或直接 lean 编译都行。

-- mini.lean
-- 只保留一个定理，先不实现，用 sorry 占位
theorem demo_add_comm (a b : Nat) : a + b = b + a := by
  sorry

同时把环境信息记下来，这三条命令的输出直接贴进记录表：

lean `--version`
lake `--version`
elan show

编译这份最小文件确认它能过（因为有 sorry，通常是警告而非错误）：

lake env lean mini.lean
# 没有 lake 工程时可以直接：
lean mini.lean

记录 Lean 版本号时建议写全，例如把 lean `--version` 的整行输出留着。不要只写“Lean 4”，因为同一大版本下引理名和策略行为也可能不同。这个最小文件的作用是排除项目复杂度干扰，让“差一步”变成可以重复触发的失败样本。

在提示词里补上 Lean 版本和可用库信息

模型不知道你本地导入了什么，也不知道你用的是哪一个 Lean 版本，它给出的最后一步常引用一个你环境里不存在的引理。提示词里把环境说清楚，比反复要求“再检查一遍”更有用。下面是一个可替换的模板，{{模型名称}} 处按实际调用的模型填写。

你是 {{模型名称}}，正在为 Lean 4 写证明。

当前环境：
- Lean 版本：{{lean `--version` 的输出}}
- 工具链标识：{{lean-toolchain 文件内容}}
- 可用导入：{{实际 import 的库，如 Mathlib / Init / Std}}
- 文件顶层已有的 open 语句：{{open 了哪些命名空间}}

要求：
1. 只使用上述导入中存在的引理，不要假设未导入的库可用。
2. 给出完整可编译的定理证明，不要留 sorry。
3. 每一步注明所用引理或策略的来源命名空间。

待证目标：
{{定理陈述}}

我当前卡住的地方：
{{上一次输出} 编译时报错信息}

注意两点：一是导入列表要写真实值，不确定就先跑一次 #check 看看；二是别把整个 Mathlib 的清单塞进去，模型对长清单的利用率有限，写清楚“Mathlib 可导入”这类范围往往更实际。写完环境后先跑一次，如果模型仍差一步，说明问题可能不在信息缺失，而更可能在版本假设上。

用相同提示词换 Lean 版本跑一次对比

判断差一步是否由版本差异导致，关键是把提示词、文件内容、导入全部冻结，只换 Lean 工具链。用 elan 管理多版本时，可以这样安装和切换（版本号请替换成你本地已有或需要的实际版本，不要凭印象填）：

# 查看已装工具链
elan toolchain list

# 安装指定版本（把 vX.Y.Z 换成实际版本号）
elan toolchain install leanprover/lean4:vX.Y.Z

# 只在当前目录覆盖，不影响全局
elan override set leanprover/lean4:vX.Y.Z

# 确认当前生效版本
lean `--version`

也可以直接用一个 lean-toolchain 文件指定版本，文件里只写工具链标识，切目录即生效。两个版本下各跑一次相同的 mini.lean 和相同的提示词，把两次的编译输出都留着。

需要提醒的是：切版本会连带影响依赖库的可用性，Mathlib 的版本与 Lean 版本通常需要匹配。如果换了版本后项目整体编不过，那就不是模型证明的问题，先把工具链与依赖对齐再谈对比。版本对比更适合在干净的最小工程里做，而不是直接在业务工程里切。

检查是否缺少 import 或打开命名空间

模型最后一步常写 Nat.add_comm 或 simp [foo] 这类引用。引理名对不对、当前文件能不能看见它，用 #check 直接验证，不要靠读代码猜。

import Mathlib

open Nat

#check add_comm
#check Nat.add_comm
#check @Nat.add_comm
#check List.length_append

执行方式与编译同一个文件一致：

lake env lean check.lean

判断规则很简单：#check 报 unknown identifier 或 unknown namespace，说明这个引理在当前 import 和 open 组合下不可见；要么补 import，要么补 open，要么让模型换用确实存在的引理名。带下划线的内部定理通常需要显式指定完整命名空间，可以先用 #check 一个个试，再回头看模型输出里那一步差在哪。

另外留意隐式参数与命名空间缩写：有的引理在 open Nat 后可写短名，没有 open 时必须写全名。模型有时默认已经 open 了某个命名空间，而你的文件没有，这一步就会直接失败。

把成功和失败输出保存下来做差异对比

收集到证据后再决定改提示词还是改环境。建议每次实验只改一个变量，其他列保持一致，表里字段如下；行数按你实际跑的版本数增加。

对比时看两个信号：同一提示词换了 Lean 版本后是否通过，说明差一步由版本差异主导；同一版本下补了版本与导入信息后是否通过，说明差一步由提示词信息缺失主导。两者都没通过，通常是引理本身在你的依赖里不存在，回到 #check 那一步继续查。

记录表不需要写得很长，但要能回答“这一次我改了哪个变量、结果变了没有”。建议把模型输出原样保存，不要只记一句“失败了”，否则下次很难判断是措辞问题还是环境问题。把最小文件、提示词、两版工具链输出和这张表放在同一个目录下，后续复盘或换模型复测都能直接复用。