第一个程序与第一个证明

def/#eval/#check、theorem 与 by、Infoview 读法，以及「错误信息怎么读」。

三个诊断命令

写 Lean 时最常用的三条命令，它们不产生任何代码，只在编辑器里给你反馈：

#eval 2 + 3          -- 5          求值
#check 2 + 3         -- 2 + 3 : Nat  查类型
#print Nat.add       --            看定义

命令	作用
`#eval`	计算表达式的值
`#check`	显示表达式的类型，不求值
`#print`	显示某个名字的定义

#check 是学 Lean 时用得最多的——遇到任何不确定的东西，先 #check 一下。

第一个程序

def hello : String := "Hello, Lean 4!"

#eval hello          -- "Hello, Lean 4!"

def 名字 : 类型 := 值。类型可以省略（Lean 会推断），但公开的定义建议写全：

def answer := 42            -- 推断为 Nat
def answer' : Nat := 42     -- 显式，更清晰

带参数：

def double (n : Nat) : Nat := n * 2

#eval double 21      -- 42

函数调用不用括号：写 double 21 而不是 double(21)。这是 ML 系语言的惯例，多参数时更明显：

def add (a : Nat) (b : Nat) : Nat := a + b

#eval add 3 4        -- 7

同类型参数可以合并写：

def add (a b : Nat) : Nat := a + b

可执行程序

def main : IO Unit :=
  IO.println "Hello from Lean!"

main 的类型是 IO Unit——一个「执行后产生副作用、返回空」的动作。Monad 那一章会讲清 IO 是什么。

lake exe myproject

第一个证明

theorem two_plus_two : 2 + 2 = 4 := by
  rfl

拆开看：

部分	含义
`theorem`	声明一个定理（与 `def` 几乎等价，见下）
`two_plus_two`	定理的名字
`2 + 2 = 4`	要证的命题——它同时是这个定理的「类型」
`:=`	「它的证明是」
`by`	进入 tactic 模式
`rfl`	一个 tactic：「两边按定义相等」

rfl 是 reflexivity（自反性）——它能证明 a = a 形式的命题，且允许两边按定义化简后相等。2 + 2 与 4 在 Nat 上定义计算后确实是同一个项，所以 rfl 成功。

theorem 与 def 的关系

def two_plus_two' : 2 + 2 = 4 := by rfl     -- 也合法！

theorem 与 def 在类型检查层面几乎相同。差别是工程性的：

theorem 的内容被标记为不可展开（proof irrelevance 相关优化），编译时不生成代码。
def 会参与计算与代码生成。

约定是：类型是命题（Prop）时用 theorem，是数据时用 def。这个区分在命题即类型一章会讲透。

两种证明模式

term 模式：直接给出证明项

theorem my_id (p : Prop) (hp : p) : p := hp

读作：「给定命题 p 和一个 p 的证明 hp，我要证 p——证明就是 hp 本身。」

这就是一个普通的函数定义。它接受参数、返回值，只不过参数是「证明」，返回的也是「证明」。

tactic 模式：用 `by` 一步步构造

theorem my_id' (p : Prop) (hp : p) : p := by
  exact hp

by 后面是一串 tactic，每条指令改变当前的证明状态，直到目标被完全解决。

两种模式可以混用：

theorem mixed (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
  ⟨hp, by exact hq⟩

实践中绝大多数证明用 tactic 模式——复杂证明写成 term 几乎不可读。

读 Infoview

这是最重要的技能。把光标放在 tactic 之间：

theorem example_state (a b : Nat) (h : a = b) : b = a := by
  -- 光标放这里，Infoview 显示：
  --   a b : Nat
  --   h : a = b
  --   ⊢ b = a
  exact h.symm

Infoview 显示的叫 证明状态（goal state）：

a b : Nat        ← 局部上下文：有哪些东西可用
h : a = b        ← 包括假设（它们也是「有类型的项」）
⊢ b = a          ← 目标：要构造一个这个类型的项

⊢ 读作 turnstile，左边是「已有的」，右边是「要证的」。

读证明状态的正确方式：「我手上有这些项，要造出一个类型为目标的项。」

注意 h : a = b 与 a b : Nat 在形式上完全一样——都是 某个名字 : 某个类型。假设与数据在 Lean 里没有本质区别，这正是「命题即类型」的直接体现。

多个目标时会依次列出，用 case 或 ·（focus dot）分别处理：

theorem two_goals (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp      -- 第一个目标
  · exact hq      -- 第二个目标

· 是圆点（U+00B7），VS Code 里输入 \. 自动补全。

Unicode 输入

Lean 大量使用 Unicode 符号。编辑器扩展提供反斜杠缩写：

输入	得到	含义
`\to` 或 `\r`	`→`	函数箭头 / 蕴含
`\and`	`∧`	合取
`\or`	`∨`	析取
`\not`	`¬`	否定
`\iff`	`↔`	当且仅当
`\forall` 或 `\all`	`∀`	全称量词
`\exists` 或 `\ex`	`∃`	存在量词
`\Nat`	`ℕ`	自然数
`\lam`	`λ`	lambda
`\<` `\>`	`⟨` `⟩`	匿名构造子
`\.`	`·`	focus dot
`\l`	`←`	反向（`rw` 用）

输入缩写后按空格或 Tab 转换。不记得某个符号怎么打：把光标放在它上面，编辑器会提示缩写。

ASCII 替代大多存在（-> 对 →、/\ 对 ∧、fun 对 λ），但社区惯例是用 Unicode。

错误信息怎么读

最常见的三类错误：

type mismatch

def bad : Nat := "hello"

type mismatch
  "hello"
has type
  String : Type
but is expected to have type
  Nat : Type

结构固定：给的是什么、它是什么类型、期望什么类型。从下往上读最快。

unknown identifier

unknown identifier 'foo'

名字拼错，或所在的模块没 import，或需要 open 某个命名空间。

unsolved goals

theorem incomplete (n : Nat) : n + 0 = n := by
  skip

error: unsolved goals
n : Nat
⊢ n + 0 = n

tactic 跑完了但目标还在。错误信息里会把剩余目标完整打印出来——这是最有用的一类错误，它直接告诉你还差什么。

Lean 的错误信息有时会很长（尤其涉及类型类推断失败或 simp 循环）。先看第一行的错误类型，再看最后的具体项，中间的展开细节通常可以跳过。

sorry

theorem hard_thing (n : Nat) : n * 0 = 0 := by
  sorry

sorry 是「先欠着」——它能通过类型检查，但会产生一个警告，且该定理会被标记为「使用了 sorry」。

它是开发过程中的重要工具：先用 sorry 把整个证明骨架搭起来，再逐个填坑。

sorry 会传染：任何用到含 sorry 定理的定理，也是不可信的。Lean 会一路标记。

检查一个定理是否真的完成，用：

#print axioms hard_thing

输出里若有 sorryAx 就说明没证完。CI 里应该检查这一点。

下一篇：类型与项。

本页目录