Lean4中替换theorem为lemma后出现语法错误的原因咨询

你原本的理解没错：在Lean4里，theorem和lemma本质上是语法同义词，仅在语义上用来区分结论的重要性——theorem用于核心结论，lemma用于辅助性的小结论，语法层面完全可以互换。

你遇到的报错并非因为lemma本身的语法问题，大概率是以下几种情况之一：

• 代码中存在不可见的特殊字符：替换关键字时可能不小心引入了零宽空格、全角符号之类的不可见字符，导致Lean4解析器无法正确识别lemma行的语法结构，进而把by当成无效标识符。
• Lean4版本兼容问题：如果使用的Lean4版本过于老旧，可能存在语法解析bug，部分旧版本对lemma := by ...的简写支持不完善，而theorem的解析逻辑更稳定。
• 编辑器/IDE缓存或语法解析错误：Lean4的IDE插件偶尔会出现缓存异常，明明代码语法正确却误报错误。

验证与解决办法 #

1. 完全手动重新输入报错的lemma代码段，确保所有符号都是英文半角，无额外不可见字符。
2. 更新Lean4到最新稳定版本，新版本修复了很多旧的解析bug。
3. 重启编辑器或清除插件缓存后重新加载代码。

你也可以用以下标准写法验证语法正确性：

inductive MyNat where
  | zero: MyNat
  | succ: MyNat → MyNat
  deriving Repr

open MyNat

def add (m: MyNat) (n: MyNat) : MyNat :=
  match n with
  | zero => m
  | succ n' => succ (add m n')

instance : Add MyNat where
  add := add

lemma add_succ (m n: MyNat) : m + succ n = succ (m + n) := by
  rfl

内容的提问来源于stack exchange，提问作者roi_saumon