准备 Lean 4 实验环境

到第 06 篇为止，本系列的所有概念都已铺开。从本篇开始换姿势：不再用 Python 模拟，也不再贴 Lean 4 片段当示意，而是让读者在自己机器上跑 Lean 4，写下第一个证明，看着编辑器右栏的 No goals 出现。

本篇是一篇短工具文：装 elan、跑 lake new、配 VS Code、写一段会动的 Lean 代码。系列从下一篇开始所有 Lean 示例都默认在这套环境里跑。

一句话总结要装什么

组件	作用	安装方式
`elan`	Lean 4 版本管理器（类似 Rust 的 rustup）	官方脚本一行
`lean`	Lean 4 编译器与类型检查器	`elan` 自动拉
`lake`	项目与依赖管理器（类似 cargo）	随 `lean` 一起
VS Code + Lean 4 插件	编辑器 + InfoView	应用商店搜 `lean4`

完全不想装本地环境的读者，可以直接用 Lean 官方 Web 编辑器 https://live.lean-lang.org/。本篇先讲本地路径，最后留 Web 编辑器的最小回退方案。

安装 elan

elan 是 Lean 的工具链管理器。它管理多个 Lean 版本，自动按项目里的 lean-toolchain 拉对应版本。

macOS / Linux：

1	`curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh`

执行过程会问要不要把 ~/.elan/bin 加入 PATH。回车默认接受即可。

装完后开新终端验证：

1
2
3

elan --version
lean --version
lake --version

elan 默认装一份当前推荐的 Lean 4 toolchain。lean --version 会输出形如 Lean (version 4.x.x, ...) 的字符串。

Windows 用户从 https://github.com/leanprover/elan/releases 拉 Windows 版本的安装脚本，或直接装预编译的 elan-init.exe。

不推荐用 Homebrew / apt 装 Lean。Lean 4 本身演进很快，配套生态（Mathlib）对版本敏感，包管理器版本经常滞后或与 lean-toolchain 不匹配。elan 是唯一稳的路径。

用 lake 起一个新工程

lake 是 Lean 4 的项目/构建/包管理器。最小工程：

1 2	`lake new formal_intro cd formal_intro`

lake 会生成下面这一棵：

formal_intro/
  lakefile.lean        # 项目定义
  lean-toolchain       # 锁定的 Lean 版本
  Main.lean            # 可执行入口
  FormalIntro.lean     # 库模块入口
  FormalIntro/
    Basic.lean         # 示例模块
  .gitignore

lakefile.lean 大致这样：

import Lake
open Lake DSL

package «formal_intro» where
  -- 配置项可选

lean_lib «FormalIntro» where
  -- 库配置

@[default_target]
lean_exe «formal_intro» where
  root := `Main

第一次跑 build：

1	`lake build`

lake 会编译 FormalIntro.Basic 和 Main，输出二进制到 ./.lake/build/bin/formal_intro。

1	`./.lake/build/bin/formal_intro`

打印 Hello, world!。整个工具链算搭通。

Mathlib 是 Lean 4 的数学/算法标准库。系列前期不依赖 Mathlib，本篇不引入；想引入时在 lakefile.lean 里加一句 require mathlib from git "https://github.com/leanprover-community/mathlib4.git" 然后 lake update。第一次拉 Mathlib 要装几分钟、占几个 GB，且对 Lean 版本严格匹配——做之前先确认 lean-toolchain 与 Mathlib lean-toolchain 一致。

配 VS Code

形式化的核心交互体验在编辑器里。装两个东西：

VS Code 本体。
应用商店搜 lean4，装 leanprover.lean4 插件。

打开 formal_intro 目录，等几秒，状态栏右下角会显示 Lean 服务器就绪。

把 FormalIntro/Basic.lean 内容改成：

namespace FormalIntro

def hello : String := "Hello, formal world!"

-- 第一条定理
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

-- 第一个用 tactic 的证明
theorem add_zero (n : Nat) : n + 0 = n := by
  rfl

end FormalIntro

打开 Lean InfoView（Ctrl/Cmd+Shift+P → “Lean 4: Infoview: Show Infoview”），把光标停在 rfl 前面，右侧应当显示：

1	`⊢ n + 0 = n`

光标移到 rfl 后面：

1	`No goals`

No goals 出现的瞬间就是"定理得证"的字面意义。Lean 4 的内核刚刚把 add_zero 这个项与它的声明类型对位检查通过。

InfoView 是核心工作面

Lean 4 不像普通编程语言用 print 调试。证明开发的全部反馈都来自 InfoView：

现象	含义
InfoView 显示 `⊢ goal`	当前位置还需要构造一个属于 `goal` 类型的项
InfoView 显示 `No goals`	所有目标已被消解，证明完成
InfoView 显示红色错误	类型或证明不匹配；细看上方 `Messages` 面板
`#check expr`	当前位置 InfoView 输出 `expr : ty`
`#eval expr`	把 `expr` 在 Lean 求值器里跑出来

把下面几条加到 Basic.lean，试着读 InfoView 反馈：

#check @And.intro          -- 看构造子签名
#check (fun h : True => h) -- 看 lambda 的推断类型
#eval (1 + 2 : Nat)        -- 输出 3
#eval (List.range 5)       -- 输出 [0,1,2,3,4]

#check 与 #eval 是写证明时最常用的探针。它们不进入最终编译产物，只在 InfoView 里报告结果。

tactic 与 term 两套写法

Lean 4 接受两种写法构造证明项：

term mode：直接给出表达式，例如 fun h => ⟨h.right, h.left⟩。
tactic mode：用 by 开头，写一段 tactic 脚本，由 Lean 自动构造出对应的项。

-- term mode
theorem and_swap_term (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

-- tactic mode
theorem and_swap_tactic (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro h
  exact ⟨h.right, h.left⟩

-- 也可以混写
theorem and_swap_mixed (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro ⟨p, q⟩
  exact ⟨q, p⟩

三种写法等价。tactic 的好处是把"构造证明"变成"渐进对话"：每写一行 tactic，InfoView 立刻更新还剩哪些子目标。复杂证明几乎必走 tactic mode。

tactic 在内部就是一段构造证明项的元程序，最终产物仍然是 term mode 的项。所以"编译通过 = 定理得证"的语义没有被绕过。

错误信息怎么读

故意写错：

1 2	`theorem broken (P Q : Prop) : P ∧ Q → Q ∧ P := fun h => ⟨h.left, h.right⟩ -- 写反了`

VS Code 红线，Messages 面板：

type mismatch
  ⟨h.left, h.right⟩
has type
  P ∧ Q : Prop
but is expected to have type
  Q ∧ P : Prop

Lean 的错误格式固定：

出错的表达式（⟨h.left, h.right⟩）。
它被推断为什么类型（P ∧ Q）。
它被期望是什么类型（Q ∧ P）。

读 Lean 错误的关键就是把"推断"和"期望"对位看，找差异。它从不会"说不出问题"，每个错误都有精确定位。

不想装环境的最小回退方案

如果不想本地装 Lean，打开 https://live.lean-lang.org/，把上面 Basic.lean 里的内容粘进去。Web 编辑器自带 InfoView，体验差不多。Web 路径的限制：

不能持久保存代码（关掉就丢，需要自己存 gist 或本地 .lean）。
不能装 Mathlib（系列前期不需要，问题不大）。
大文件慢，因为整套 Lean 在浏览器里跑。

Web 编辑器适合"看系列文章顺手跑一个示例"。要真正写证明、组工程、引依赖，还是回到本地 lake 工程。

项目骨架推荐

读完系列建议在自己机器里维护一个 formal_intro 工程，按章节分文件：

formal_intro/
  lakefile.lean
  lean-toolchain
  FormalIntro/
    Basic.lean              # 当前文件
    Curry_Howard.lean       # 系列 02 同构例子
    Stlc_Theorems.lean      # 系列 03 STLC 定理
    Dependent.lean          # 系列 05 Π/Σ 示例
    Induction.lean          # 系列 06 归纳证明
    First_Theorems.lean     # 系列 08 经典命题

每个文件顶上：

1
2
3

namespace FormalIntro.Curry_Howard
-- ... 你的代码 ...
end FormalIntro.Curry_Howard

namespace 隔离避免命名冲突。lake build 会按依赖图编译，改动一个文件不必重编全部。

检查清单

写下一篇之前，请确认能跑完以下动作：

[ ] lake build 在 formal_intro 工程里成功。
[ ] 在 VS Code 中打开 Basic.lean，InfoView 能显示 add_zero 的目标和 No goals。
[ ] 故意写一个类型错误，能在 Messages 面板看到"推断 vs 期望"格式的错误。
[ ] 能区分 #check 与 #eval。
[ ] 知道 theorem 与 def 在 Lean 4 内部几乎等价，只区分目标宇宙。

模式提炼

模式	内容
工具链管理用 `elan`	不要用包管理器版本；项目级 `lean-toolchain` 锁版本
项目骨架用 `lake new`	标准结构有 lakefile、lib、入口、库目录
反馈来自 InfoView	证明开发不靠 `print`；目标态、错误、`#check` 都在右栏
term / tactic 等价	tactic 是构造项的元程序，最终产物仍是 term
错误是"推断 vs 期望"	读错误的固定姿势

给读者的练习

在 Basic.lean 中加一条 theorem identity : ∀ {α : Type} (x : α), x = x := fun _ => rfl，看 InfoView 怎样显示其类型。
把上一篇 add 函数重写成 Lean 版（已是 Lean 版，把它放进自己的工程跑过 #eval add 2 3 看输出）。
试 tactic 模式下的 apply、exact、rfl、intro 四个最基础的 tactic，分别在 InfoView 里观察目标的变化。
故意 import Mathlib（先不要真 require），看 Lean 报什么错——读 Lean 的依赖错误是常见调试场景。

衔接到下一篇

环境搭好了。下一篇真在 Lean 里证一组经典命题：And.comm、Or.comm、Nat.add_comm、List.length_append、reverse_reverse。每条命题都有 term mode 与 tactic mode 两种写法。读完那一篇，"在 Lean 4 里写一段非平凡证明"对读者来说就不再是抽象概念。

参考资料

Lean 官方主页：https://lean-lang.org/
Lean 4 文档：https://leanprover.github.io/theorem_proving_in_lean4/
Functional Programming in Lean. https://leanprover.github.io/functional_programming_in_lean/
elan GitHub：https://github.com/leanprover/elan
Lake 文档：https://github.com/leanprover/lake
Lean Web 编辑器：https://live.lean-lang.org/
Lean 社区主页：https://leanprover-community.github.io/