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語言證明一些數學定理。