lean-mcp

请使用 lean-mcp 编译并验证下面的 Lean 4 代码，指出报错位置并给出可通过的修改建议：
lean
import Mathlib

theorem add_zero_example (n : Nat) : n + 0 = n := by
  simp

返回编译结果、是否验证通过，以及必要的报错说明或修改建议。

请用 lean-mcp 检查这段 Lean 4 证明失败的原因，逐条解释 tactic 为什么不成立，并提供修正版：
lean
import Mathlib

theorem wrong_example (a b : Nat) : a + b = b + a := by
  rfl

给出失败原因、错误上下文，以及可编译通过的替代证明。

请使用 lean-mcp 验证下面代码是否正确引用并使用 Mathlib，如果不正确请补全 import 或改写证明：
lean
import Mathlib

theorem list_len_nil : List.length ([] : List Nat) = 0 := by
  rfl

说明依赖是否充分、代码能否通过，并给出最终可运行版本。