Lean - 维基百科，自由的百科全书

Lean

编程范型	函數式、指令式
實作者	Lean FRO
发行时间	2013年，​11年前​（2013）
当前版本	4.14.0（2024年12月1日；穩定版本）[1]
型態系統	靜態、強型、推論
實作語言	Lean , C++
操作系统	跨平台
許可證	Apache License 2.0
網站	lean-lang.org
啟發語言
ML Coq Haskell

Lean是一款在含歸納類型的構造演算基礎上所開發的電腦證明助手（英语：Proof assistant）和函數式編程語言。^[2]Lean最初由萊昂納多·德·莫拉（英语：Leonardo de Moura）在微軟研究院下研發，目前以開源合作計劃的形式刊登在GitHub上。2023年成立的非盈利Lean集中研究組織（英語：Lean Focused Research Organization，縮寫Lean FRO）支持Lean的持續開發。

2013年，當時在微軟研究院工作的萊昂納多·德·莫拉發佈函數式編程語言Lean。^[3]早期版本（後來被稱為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當中，程式速度從而得以提高。^[2]Lean 4的宏系統、類型類合成系統和記憶體管理系統都比前一版本大幅改善。

Lean 4的代碼語法有所改變，因此與Lean 3不向下兼容。^[4]

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

Lean的官方軟件包包含一個名為std4的標準庫，內含數學證明及普通軟件開發中一些常用的數據結構。^[6]

2017年，Lean社群創立mathlib函式庫，目的是將盡可能多的純數學概念以Lean語言數碼化地寫下來，以龐大的單一函式庫的形式來維護，一直攀登至當今數學研究的前沿。^[7][8]截至2024年6月21日 (2024-06-21)^[update]，mathlib已形式化超過15萬項定理、近8萬項定義。^[9]

Lean支援與以下編輯器整合使用：^[10]

• Visual Studio Code，通過lean4附加項
• Neovim，通過lean.nvim附加項
• Emacs，通過lean-mode模式

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

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

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

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

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受到了托馬斯·黑爾斯^[11]和凱文·巴扎德（英语：Kevin Buzzard）^[12]等數學家的重視。黑爾斯在他的「形式抽象」（英語：Formal Abstracts）計劃中用到Lean語言。^[13]巴扎德則通過他的「齊娜計劃」（英語：Xena Project），希望用Lean寫下倫敦帝國學院本科數學課程內容中的每一項定理。^[14]

2021年，在菲爾茲獎得主皮特·舒爾策的慫恿下，一組數學家利用Lean形式化舒爾策在凝聚態數學（英语：condensed mathematics）範疇的一篇證明，證實了它的正確性。這項計劃成功形式化位於研究最前沿的數學成果，受到了廣泛關注。^[15]2023年，菲爾茲獎得主陶哲軒利用Lean形式化多項式弗賴曼-魯饒猜想（英语：Freiman's theorem）（英語：Polynomial Freiman-Ruzsa conjecture）的一項證明，該項證明同年發表在陶哲軒等人的一篇論文當中。^[16]

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

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

• 類型論
• 依賴類型

• Lean官方網站
• Lean社群網站
• Lean FRO
• 自然數遊戲：Lean互動教程