第一个证明

做完这一节，你会写出一条被 Lean 接受的定理，并且看懂它的每一个词。

打开上一节的 Test.lean，或者在线版 live.lean-lang.org，把下面的代码一段一段敲进去。

学完你能做什么

• 分清“让 Lean 算”和“让 Lean 证”
• 写出 theorem 名字 : 命题 := by 证明 这个结构
• 看懂 Lean 拒绝一个错误命题时说的话

第 1 步：让 Lean 算

#eval 2 + 2

你应该看到：

4

#eval 是“算一下这个式子”。它运行程序，给出结果。

• 我看到了 4

第 2 步：让 Lean 证

把“2 + 2 等于 4”写成一条定理：

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

你应该看到：没有报错，也没有任何输出。在 Lean 里，证明通过就是安静。

逐词读一遍：

写的是	意思
theorem	下面是一条定理
two_plus_two	它的名字，随你起
: 2 + 2 = 4	冒号后面是命题，也就是你声称成立的那句话
:= by	接下来用一步步的“策略”来证明
rfl	一个策略：两边各自算出来，结果一模一样，所以相等

确认一下 Lean 记住了它：

#check two_plus_two

你应该看到：

two_plus_two : 2 + 2 = 4

#check 问的是“这个东西是什么”。回答是：two_plus_two 是命题 2 + 2 = 4 的一个证明。

• 我的 two_plus_two 没有报错，#check 显示出了它的命题

第 3 步：试着证一句假话

把 4 改成 5，看 Lean 怎么说：

theorem two_plus_two_wrong : 2 + 2 = 5 := by
  rfl

你应该看到：rfl 下面出现红色波浪线，报错里有这一句：

is not definitionally equal to the right-hand side

意思是：左边算出来的东西和右边不是同一个。Lean 没有被说服，这条“定理”不成立，后面也不能使用它。

换一个策略也一样。decide 会直接把命题算出真假：

example : 2 + 2 = 5 := by
  decide

Tactic `decide` proved that the proposition
2 + 2 = 5
is false

这里的 example 和 theorem 一样，只是不起名字，适合随手试。

• 我亲眼看到了 Lean 拒绝 2 + 2 = 5

考考你`#eval 2 + 2` 和 `theorem two_plus_two : 2 + 2 = 4 := by rfl` 的区别是什么？

检查点

• 我能写出 theorem 名字 : 命题 := by 这个结构
• 我知道证明通过时 Lean 什么都不输出
• 我知道 rfl 证的是“两边算出来一样”
• 我知道 example 是不起名字的 theorem

没成功？

敲完没有任何反应，也没有红线。 检查文件名是不是以 .lean 结尾，以及工具链是不是还在后台安装。

theorem 那一行报“已经声明过”。 同一个文件里名字不能重复。换个名字，或者用 example。

下一节

2 + 2 = 4 靠算就能证。大多数命题不行，比如“如果 p 成立就有 q，现在 p 成立，所以 q 成立”。下一节开始学真正的推理。