Leanstral 1.5 在 Lean 4 里报错——是策略用错还是缺少导入？

模型给出的 Lean 4 证明报错时，先用报错文本本身做一次分流：如果错误落在引理名、命名空间或 tactic 名上，通常先怀疑 import / open 缺失；如果错误落在目标状态、类型匹配或“策略没有进展”上，通常先怀疑策略与当前目标不匹配。两类问题会互相伪装——例如某个 hypothesis 名字报 unknown identifier，其实是因为前一步策略没跑成功、根本没引入该假设。所以判断顺序是：先复制报错原文，再看符号可见性，最后才逐条试策略。

遇到 Leanstral 1.5 生成的证明在 Lean 4 报错，不要先改策略。把报错文本原样复制出来：unknown identifier / unknown namespace / unknown tactic 多半是 import、open 或 tactic 库没加载；tactic failed、unsolved goals、type mismatch、application type mismatch 多半是策略用错或对目标理解有偏差。用 #check 验证可见性，用 trace_state 拆步定位，改完再跑 lake build。环境版本与编辑器不一致时，结论要重新确认。

复制 Lean 报错信息，定位是 unknown identifier

把终端或编辑器里的报错整段复制，不要只截最后一行。Lean 4 的报错会带上文件、行号、列号和上下文，这些信息决定了往哪个方向查。

第一类报错指向导入或命名空间缺失，典型文本形如：

unknown identifier 'Nat.dvd_gcd'
unknown namespace 'Foo'
unknown tactic 'positivity'

这类错误的共同点是：报错位置出现在“名字”上，而不是出现在目标或类型上。适用场景是模型引用了某个库里的引理或 tactic，但当前文件没有把它带进来。操作动作是先在该行前后确认是否 import Mathlib（或更细的 import Mathlib.Tactic、import Mathlib.Data.Nat.GCD.Basic 之类），再确认符号是否被 open 到当前作用域。

第二类报错指向策略与目标不匹配，典型文本形如：

tactic 'simp' failed, no progress
unsolved goals
type mismatch / application type mismatch
no goals to be solved

这类错误的共同点是：名字本身是认识的，但策略在当前目标上没有产生预期效果。风险边界在于，仅凭报错文本无法百分百区分，最终还是要靠 #check 和逐行运行来确认。

检查证明文件头部是否缺少 import 或 open

在文件顶部临时插入几行 #check，这是判断“模型引用的引理在当前文件里是否可见”的最直接办法。放在 import 之后、定理之前即可：

import Mathlib

#check Nat.dvd_gcd
#check Finset.sum_comm
#check Nat.succ_eq_add_one
open Nat
open scoped BigOperators

-- 之后再写模型给的定理

如果 #check 报 unknown identifier，说明这个引理名在当前 import 组合下不可见，需要补 import、换用正确名字，或者确认它是否存在于你锁定的 Mathlib 版本里。如果 #check 正常打印类型，而定理体内同一名字仍报 unknown identifier，则要怀疑是命名空间没打开，或该名字被局部变量遮蔽。

再补一个保守做法：在排查阶段打开 set_option autoImplicit false。它会禁止 Lean 自动把未声明的标识符当成隐式变量，从而把拼写错误、漏引入的名字提前暴露出来。验证方式是加回这一行后重新编译，看报错数量是否变化；如果变化很大，说明原证明依赖了自动隐式变量，这本身就是一类隐患。

Leanstral 1.5 在 Lean 4 里报错——是策略用错还是缺少导入？

把模型给的策略拆成单步，逐步运行 Lean

模型往往一次给出多行 tactic。定位失败点时，把 by 块里的每一行拆开，配合 trace_state 观察目标变化。示意结构如下：

example (n : Nat) : n + 0 = n := by
  trace_state
  induction n with
  | zero => rfl
  | succ k ih =>
    trace_state
    simp [Nat.succ_eq_add_one, ih]

操作顺序是：先只保留第一行加 trace_state，编译一次，看 Lean 打印的目标；再加第二行，再编译一次。哪一行加上之后目标不再变化、或开始报 unsolved goals，问题就定位到那一步。

为了让中间步骤能单独通过编译，可以临时用 sorry 占位未完成的分支。需要说明的是，sorry 只是排查用的临时占位，最终提交前必须替换掉，否则文件里会留下未证明的洞。适用场景是模型策略较长、你无法肉眼判断哪一步失效；验证方式是每加一行就编译并对比目标文本。

对比同一目标下不同策略的报错差异

判断到底是模型策略问题还是目标理解偏差，可以用同一个目标分别套两条候选策略，各自单独放在一个 example 里编译，逐条记录“目标状态 + 错误信息”：

example (a b : Nat) (h : a <= b) : a + 0 <= b := by
  omega

example (a b : Nat) (h : a <= b) : a + 0 <= b := by
  linarith

记录时至少写三项：编译前 trace_state 打印的目标、该策略的错误原文、错误是否出现在名字上。若两条策略都报 unknown identifier 或 unknown tactic，问题在环境与导入，不在策略选择；若两条策略都报 tactic ... failed，说明目标本身可能被理解错了，比如模型假设的是整数而实际变量是自然数，或假设方向反了；若一条通过、一条失败，则目标没问题，是策略选择的问题。不要预设哪条一定成功，以实际编译输出为准。

把修正后的导入和策略写回文件并重新编译

确认修法后，把 #check、trace_state、临时的 sorry 清理掉，保留真正需要的 import 和 open，再替换失效的策略，然后整体编译：

lake build

如果只想先验证单个文件，可以用 lake env lean YourProject/Proof.lean，这能确保用的是项目锁定的 toolchain 而不是编辑器自带的 Lean。整体构建通过后，再回头删掉排查期的辅助行，最后再跑一次 lake build 确认无新增报错。

一个常见的边界情况：编辑器里 #check 正常，但 lake build 报 unknown identifier，这通常说明编辑器用的根目录或 toolchain 与项目不一致。可以先确认 lean-toolchain、lakefile.lean、lake-manifest.json 三处版本是否自洽，Mathlib 依赖更新后按项目惯例执行缓存拉取命令，再重新构建。这一步不做，前面关于导入缺失的判断可能全部是假象。