1 前言

第一次听闻Lean语言，是浏览到一则关于数学家陶哲轩的报导————他借助Lean语言纠正了自己在论文中犯下的错误。

数学是一门严谨的学科，但是人们通常用自然语言作为数学的载体，这使得错误的发生难以避免。就算像陶哲轩一样的数学家，也偶有疏失。

编写编程语言并通过编译的过程就好比编写数学证明并通过程序的检查。使用编程语言作为数学证明的载体，就能允许引入对证明过程的形式化检查，减少出错的可能。

学习Lean后，我尝试证明了一些命题。我发现Lean语言是一个很有意思的工具，但是它并不容易上手。

正常来说，人们是先学会\(1+1=2\)，然后才学习阿贝尔群；先学习微积分、概率论，然后才学习测度论。使用常见的数学工具并不需要你掌握更深层的数学知识。但做数学定理的形式化时，总需要用户对一些更底层的理论有所了解。数学理论的形式化往往是一个查找API手册的过程，你得翻一翻Mathlib文档，看看这个定理可能是什么名字，是不是在Mathlib中有现成可用的证明。你编写的形式化证明可能会比自然语言更冗长，可读性差。这是我目前感受到的比较不好的体验。但总的来说，我还是对这类型的工作感兴趣，因为这仍然是一个开拓视野的，很有启发性的过程。

从这篇笔记开始，我会陆续记录和更新一些在学习和使用Lean语言中我掌握的知识和经验，希望对读者有用。

2 环境安装

和Python、Javascript等脚本语言不同，Lean 4并没有内置一个交互式的REPL（Read-Eval-Print Loop）程序。官方推荐使用VSCode等编辑器来交互式地编写Lean 4程序。推荐读者阅读Get started with Lean，根据文档配置好环境。

如果生活在中国大陆，你可能需要先配置好代理地址，才能安装Lean。 例如，

export http_proxy=127.0.0.1:7890
export https_proxy=127.0.0.1:7890
# 请根据你的具体代理设置完成👆以上配置。

然后执行

bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:stable || (echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")'

如果顺利的话，该代码将会下载安装elan和lean程序，把它们放在~/.elan/bin. 你可能需要重新启动shell，或者关闭重连VSCode来使用Lean。

执行以下命令

lean --version

如果你看到程序打印了Lean的版本，说明Lean的安装成功了。 如果elan下载的lean不是你需要的版本，你可以执行

elan toolchain install leanprover/lean4:v4.15.0

这里假设4.15.0是你想要的版本。

elan default leanprover/lean4:v4.15.0

执行上面这条语句可以将指定的版本设置为默认。

#eval Lean.versionString  -- 请检查你的Lean版本，看看是否和预期的一致。

#eval "Hello, World!"     -- 像这样处于两条横杆右边的是行内注释

👆这就是Lean语言的Hello world程序。将它保存在一个以.lean为后缀的文本文件中，如果环境配置正常，你会在VsCode的Lean Infoview页面中看到输出。

在Lean中，–符号右侧的文本是行内注释；成对的/-和-/符号包裹住的是多行注释。

3 参考资料

除了看本人的笔记，你也可以参考这些资料

• Theorem Proving in Lean：这本书比较适合那些喜欢在使用电器之前，完整地将说明书过一遍的人。
• Methematics in Lean：适合那些希望立即能将Lean用于数学问题的人。遗憾的是这本书现在还难称完整。

本系列文章在很大程度上参考了这些文章。

4 自动证明器

虽然Lean也可以作为通用编程语言来使用，但其核心功能和设计目标主要还是作为数学领域的自动证明器。

下面的例子展示了自动证明器的工作。

example : 1 + 1 = 2 := by simp  -- 证明了1 + 1 = 2

在上面的例子中，simp是Lean的自动证明策略，能辅助我们完成一些简单证明。

除了使用自动证明器，我们也可以显式地引用现有的命题来构造证明。例如：

example : 1 = 1 := rfl -- 引用`rfl`命题

这里我们引用了rfl，即自反律。自反律表明任何值都于自身相等。

在深入介绍自动证明技巧之前，我们先认识一下Lean语言中的一些基础概念。

5 基础类型

在类型理论中，每个表达式都有对应的类型（type）。

Lean的Nat类型是一个具有无限精度的无符号整数类型。当你在Lean中写下一个正整数但不指定类型时，Nat是默认类型。

#eval 1 - 2  -- 0
#check 1 - 2 -- Nat

在上面的代码中，eval指令用于求值，而check指令检查值的类型。注意当计算1 - 2时，因为使用的是Nat类型，所以返回值会被截断为0.

Nat类型能存储任意大的自然数：

-- 就算是这么大的一个数也能正常存储，这是Lean语言区别于Python、C等通用编程语言的一点。
#eval (9876543210987654321098765432109876543210 : Nat)

Nat也可以写成ℕ, 用\N即可在受支持的编辑器中打出ℕ符号。

#check Nat
-- 在文件开头使用import Mathlib.Data.Nat.Defs后，你便能使用ℕ代表Nat。
-- #check ℕ

Lean也提供了Int类型，表示整数。与Nat相同，Int类型同样是无限精度，无溢出的。

#eval -1     -- -1
#check -1    -- Int
#eval (1 - 2 : Int)
#check (1 - 2 : Int)
#eval (9876543210987654321098765432109876543210 : Int)

类似C、Python等编程语言，Lean作为一种通用编程语言，当然也提供了有限精度的整形、浮点型。

#check (255 : UInt32)
#check (-255 : Int32)
#check (0.5 : Float)

（意外的是，作为常见的基础类型，Int32在我编写本文时前几个月才作为新功能进入Lean 4😂 可见Lean 4距离成熟的通用编程语言还有距离。）

Lean也提供了Bool类型，表示布尔值。

#check (False : Bool)

6 类型的组合

新类型可以由旧类型组合而来。例如设a和b为旧类型，那么可以构造类型a -> b或者a → b来表示一个从a映射到b的函数，a × b表示由a中的元素和b中的元素构成的二元组，这也被称为笛卡尔积（Cartesian product）。笛卡尔积也可以通过Prod函数得到：

#check Prod Nat Nat

Lean允许使用Unicode字符。可以通过输入\to或\r得到→，通过输入\a \b \g得到α β γ，通过输入\times得到×.

section
  variable (a b c α β γ : Nat)
  -- 自然数到自然数的映射
  #check Nat → Nat
  -- 两种笛卡尔积的表示方式
  #check (Nat × Nat)
  #check Prod Nat Nat
end

上面的代码中，section和end的使用是为了限制variable的范围。在section结束后，我们就不能再使用a b c α β γ等变量了。

#eval Nat.add 1 1
#check Nat.add

#check Nat.add     -- 是一个函数
#check Nat.add 1   -- 还是函数
#check Nat.add 1 1 -- 是一个自然数

def add_one := Nat.add 1
#eval add_one 1

#check Nat         -- Nat : Type
#check Bool        -- Bool : Type
#check Nat -> Bool -- Nat → Bool : Type
#check Nat × Nat   -- Nat × Nat : Type

#check Type        -- Type : Type 1
#check Type 1      -- Type 1 : Type 2
#check Type 2      -- Type 2 : Type 3
#check Type 3      -- Type 3 : Type 4

#check List

#check Prod

namespace a
  universe u
  def F (α : Type u) : Type u := Prod α α
  #check F
end a

namespace b
  def F.{u} (α : Type u) : Type u := Prod α α
  #check F
end b

7 函数定义与求值

Lean可以使用fun或λ关键词创建函数：

#check fun (x : Nat) => x + 5   -- Nat → Nat
#check λ (x : Nat) => x + 5     -- λ and fun mean the same thing
#check fun x => x + 5     -- Nat inferred
#check λ x => x + 5       -- Nat inferred

给函数传入参数即可求值：

#eval (λ x : Nat => x + 5) 10
#eval (fun x : Nat => x + 5) 10

请注意理解这个例子：下面两个函数的类型都是Nat → Bool → Nat

#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2
#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2

第一个函数接收一个自然数x，然后返回一个函数，该函数接收一个布尔值y，然后返回一个自然数。因此其类型为Nat → Bool → Nat，本质上与第二个接收多个参数函数的类型相同。

8 定义和局部定义

定义使用def关键词，局部定义使用let关键词。我们可以在函数内使用局部定义，例如

def NatAdd (a : Nat) (b : Nat) :=
  let f := (λ (x : Nat) => a + x)
  (f b)
#eval NatAdd 1 2

上面的例子中，f是一个局部定义的函数，可以在NatAdd函数的后续计算中使用。

9 归纳类型

在Lean4中，归纳类型（inductive type）是一种通过列举构造函数定义的类型。

最简单的归纳类型是枚举类型。下面的Weekdy类型包含七种可能的值，对应于一周的七天。它们的区别仅在于构造函数的不同。

inductive Weekday where
  | sunday : Weekday
  | monday : Weekday
  | tuesday : Weekday
  | wednesday : Weekday
  | thursday : Weekday
  | friday : Weekday
  | saturday : Weekday

#check Weekday.sunday
#check Weekday.monday

作为归纳类型Weekday的构造函数，它们被定义在名为Weekday的命名空间下。只要使用open指令打开对应的命名空间，我们就可以直接使用构造函数的名称。

open Weekday

#check sunday
#check monday

对于归纳类型，我们可以使用match语句，对归纳类型中的每个构造函数进行匹配。

def numberOfDay (d : Weekday) : Nat :=
  match d with
  | sunday    => 1
  | monday    => 2
  | tuesday   => 3
  | wednesday => 4
  | thursday  => 5
  | friday    => 6
  | saturday  => 7

实际上自然数也可以用枚举类型表示。print指令可以打印类型的定义。

#print Nat

输出为：

inductive Nat
  | zero : Nat
  | succ (n : Nat) : Nat

可以看到实际上Nat是一种归纳类型。Nat（自然数）是这样定义的： 1. 0是一个自然数 2. 对于任意一个自然数n，succ n是n的“下一个数”，也是一个自然数

至此，本文介绍了一些Lean语言中的基础概念。后续文章将介绍如何应用Lean语言证明一些数学定理。