Lean 入门

什么是形式化验证

Lean的核心思想是将证明转换成可以被检查的对象，而lean就是负责检查其正确与否的工具。

安装

先装基础依赖：

1
2

sudo apt update
sudo apt install -y git curl

然后安装 elan：

1

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

安装过程中如果让你选择，选默认的：

1

1) Proceed with installation (default)

装完后，让当前 terminal 立即加载环境：

1

source "$HOME/.elan/env"

然后检查：

1
2
3

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

elan 会放在 ~/.elan 下，并负责管理 lean 和 lake；项目里的 lean-toolchain 还能让它自动切换所需的 Lean 版本。

确认装到了哪里：

1
2
3

which elan
which lean
which lake

测试

先建个最简单的目录：

1
2
3

mkdir -p ~/lean-test
cd ~/lean-test
nano Test.lean

写：

1
2
3
4

#eval 2 ^ 5

example (n : Nat) : n + 0 = n := by
  simp

然后：

1

lean Test.lean

应该看到：

1

32

这一步只测试纯 Lean，不涉及 Mathlib。

Basics

模块

import:

1
2
3

import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.RingTheory.Real.Irrational
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

open:

类似C++里的using namespace。

1
2

open Real BigOperators
open scoped Nat

注释

1

-- 单行注释

1
2
3
4

/-
多行
注释
-/

以及：

1
2

/-- The sequence `u` ... -/
def SequenceHasLimit ...

/-- ... -/ 是 documentation comment，类似 JavaDoc / docstring。

还有：

1
2
3
4

/-!
# How does Lean help you?
...
-/

通常用于整个 section/module 的文档。

数学符号

如果用VS Code + Lean 4 插件的话，通常是输入反斜杠开头的缩写，然后按空格或 Tab，编辑器会把它转换成 Unicode 数学符号。

\#check

判断expression的类型。

例如：

1

#check fun n m : ℕ ↦ n + m

它的类型是：

1

ℕ → ℕ → ℕ

\#eval

执行代码。

比如：

1

#eval 2 + 3

结果是：

1

5

1
2
3
4
5

#eval do
  let mut sum := 0
  for j in List.range 101 do
    sum := sum + j ^ 2
  return sum

1

#eval ∑ j ∈ Finset.range 101, j ^ 2

注意：List.range n 是一个有顺序、可重复的列表；Finset.range n 是一个有限集合，不关心顺序、没有重复元素。

证明

example

example = 匿名theorem。

example ... := by：

1
2

example : 2 + 2 = 4 := by
  rfl

theorem

1
2

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

这里 add_example 是你自定义的名字。之后可以引用：

1

#check add_example

Sorry

1
2

:= by
  sorry

相当于告诉 Lean：我暂时不证明，请假装这里有证明。

类似Python里的pass。