Lean自然数游戏Advanced Multiplication Level2报错：invalid 'begin-end'表达式

你的代码逻辑是正确的（已经显示no goals证明了目标），但触发语法错误的核心原因是Lean的begin-end块不允许存在无内容的空行。

Lean的tactic解析器会把空行误认为是begin-end块的结束标记，导致空行后的exfalso、apply等语句被当成块外代码，从而抛出语法错误。

修复后的代码 #

cases a at h,
left,
refl,
cases b at h,
right,
refl,
left,
rw mul_succ at h,
rw add_succ at h,
exfalso,
apply succ_ne_zero (succ a * b + a),
exact h,

关键注意事项 #

• 保持begin-end块内的tactic语句连续，不要插入无意义的空行
• 确保每个tactic语句结尾的逗号正确（你的代码里逗号都没问题，空行是唯一问题）
• 即使逻辑上已经完成证明（显示no goals），语法错误仍会阻止关卡提交，必须先修正语法问题

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