Lean

Lean是一款在含歸納類型的構造演算基礎上所開發的電腦證明助手和函數式編程語言。Lean最初由在微軟研究院下研發，目前以開源合作計劃的形式刊登在GitHub上。2023年成立的非盈利Lean集中研究組織（，縮寫Lean FRO）支持Lean的持續開發。

歷史
2013年，當時在微軟研究院工作的萊昂納多·德·莫拉發佈函數式編程語言Lean。早期版本（後來被稱為Lean 1和2）純粹為實驗版本，當時支援的同倫類型論數學基礎在後來的版本中不再支援。

2017年1月20日發佈的Lean 3是Lean的首個穩定版本。Lean 3主要是以C++實現，某些功能則是以Lean語言本身實現。3.4.2版之後，Lean 3正式退役，Lean 4版開發工作開始。Lean 4開發期間，由於青黃不接，Lean社群因此自行開發了非正式版本，直到3.51.1版。

2021年，Lean 4正式發佈。該版本將整個Lean語言以Lean本身重新實現，增加了更強大高效的元編程功能。用Lean寫的元程式能夠編譯成C語言代碼，再反過來以插件的形式載入到Lean當中，程式速度從而得以提高。

2023年，Lean集中研究組織成立，目的是改善Lean語言的可擴展性和用戶體驗，以及實現自動化定理證明。

概論
函式庫
Lean的官方軟件包包含一個名為的標準庫，內含數學證明及普通軟件開發中一些常用的數據結構。

2017年，Lean社群創立函式庫，目的是將盡可能多的純數學概念以Lean語言數碼化地寫下來，以龐大的單一函式庫的形式來維護，一直攀登至當今數學研究的前沿。，已形式化超過15萬項定理、近8萬項定義。

編輯器整合
Lean支援與以下編輯器整合使用：

• Visual Studio Code，通過附加項
• Neovim，通過附加項
• Emacs，通過模式

Lean是利用客戶端附加項和語言伺服器協定來和編輯器對接的。

Lean原生支援代碼中含有Unicode字符，以便輸入各種數學符號。當利用支援的編輯器時，可用類似於LaTeX的代號輸入特殊符號，例如會自動轉換為乘號。Lean也可以編譯成JavaScript，通過瀏覽器即可實時編程。

Lean 4代碼范例
自然數可以在皮亞諾公理的基礎上以歸納類型定義。任何一個自然數要麼是零，要麼就是某另一個自然數的後繼：

inductive Nat : Type
| zero : Nat
| succ : Nat → Nat

要定義自然數之間的加法，須用模式匹配遞歸定義：

def Nat.add : Nat → Nat → Nat
| n, Nat.zero => n -- n + 0 = n
| n, Nat.succ m => Nat.succ (Nat.add n m) -- n + succ(m) = succ(n + m)

Lean支援兩種定理證明模式。一是「項模式」（），以普通的函數複合語法表達定理。二是「策略模式」（），以一行行指令的方式調用自動化證明工具，互動證明定理。以下範例使用策略模式證明「邏輯和是個對稱關係」這一命題：

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
intro h -- 假設 p ∧ q 成立，設 h 為其證明，此時目標是 q ∧ p
apply And.intro -- 將目標拆成 q 和 p 兩個目標
· exact h.right -- 第一個子目標可以用 h : p ∧ q 的右半部滿足
· exact h.left -- 第二個子目標可以用 h : p ∧ q 的左半部滿足

同一命題用項模式（連同模式匹配功能）可如下證明：

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
fun ⟨hp, hq⟩ => ⟨hq, hp⟩

應用
數學
Lean受到了托馬斯·黑爾斯和巴扎德則通過他的「齊娜計劃」（），希望用Lean寫下倫敦帝國學院本科數學課程內容中的每一項定理。

2021年，在菲爾茲獎得主皮特·舒爾策的慫恿下，一組數學家利用Lean形式化舒爾策在範疇的一篇證明，證實了它的正確性。這項計劃成功形式化位於研究最前沿的數學成果，受到了廣泛關注。2023年，菲爾茲獎得主陶哲軒利用Lean形式化（）的一項證明，該項證明同年發表在陶哲軒等人的一篇論文當中。

人工智能
2022年，人工智能公司OpenAI開發出一個可以利用Lean證明定理的神經網絡，利用大型語言模型撰寫高中級別數學奧林匹克競賽題的證明。

同年，Meta旗下的Meta AI也開發出一款人工智能模型，能夠自動解答十道國際數學奧林匹克競賽題，供公眾在Lean環境下免費使用。

參見

• 類型論
• 依賴類型

參考資料
外部連結

• [https://leanprover.github.io/ Lean官方網站]
• [https://leanprover-community.github.io/ Lean社群網站]
• [https://lean-fro.org Lean FRO]
• [https://adam.math.hhu.de/#/g/leanprover-community/nng4 自然數遊戲：Lean互動教程]