Lean
Lean是一款在含歸納類型的構造演算基礎上所開發的電腦證明助手和函數式程式語言。[2]Lean最初由萊昂納多·德·莫拉在微軟研究院下研發，目前以開源合作計劃的形式刊登在GitHub上。2023年成立的非盈利Lean集中研究組織（英語：Lean Focused Research Organization，縮寫Lean FRO）支援Lean的持續開發。
 | |
| 編程範型 | 函數式、指令式 |
|---|---|
| 實作者 | Lean FRO |
| 面市時間 | 2013年 |
| 目前版本 |
|
| 型態系統 | 靜態、強型、推論 |
| 實作語言 | Lean , C++ |
| 作業系統 | 跨平台 |
| 許可證 | Apache License 2.0 |
| 網站 | lean-lang |
| 啟發語言 | |
| ML Coq Haskell | |
歷史
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的官方軟體包包含一個名為std4的標準庫，內含數學證明及普通軟體開發中一些常用的數據結構。[6]
2017年，Lean社群創立mathlib函式庫，目的是將盡可能多的純數學概念以Lean語言數位化地寫下來，以龐大的單一函式庫的形式來維護，一直攀登至當今數學研究的前沿。[7][8]截至2024年6月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，通過瀏覽器即可實時編程。
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支援兩種定理證明模式。一是「項模式」（英語：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]和凱文·巴扎德[12]等數學家的重視。黑爾斯在他的「形式抽象」（英語：Formal Abstracts）計劃中用到Lean語言。[13]巴扎德則通過他的「齊娜計劃」（英語：Xena Project），希望用Lean寫下倫敦帝國學院本科數學課程內容中的每一項定理。[14]
2021年，在菲爾茲獎得主皮特·舒爾策的慫恿下，一組數學家利用Lean形式化舒爾策在凝聚態數學範疇的一篇證明，證實了它的正確性。這項計劃成功形式化位於研究最前沿的數學成果，受到了廣泛關注。[15]2023年，菲爾茲獎得主陶哲軒利用Lean形式化多項式弗賴曼-魯饒猜想（英語：Polynomial Freiman-Ruzsa conjecture）的一項證明，該項證明同年發表在陶哲軒等人的一篇論文當中。[16]
人工智慧
2022年，人工智慧公司OpenAI開發出一個可以利用Lean證明定理的神經網路，利用大型語言模型撰寫高中級別數學奧林匹克競賽題的證明。[17]
同年，Meta旗下的Meta AI也開發出一款人工智慧模型，能夠自動解答十道國際數學奧林匹克競賽題，供公眾在Lean環境下免費使用。[18]
參見
參考資料
- ^ Release 4.12.0. 2024年10月1日 [2024年10月22日].
- ^ 2.0 2.1 Moura, Leonardo de; Ullrich, Sebastian. Platzer, André; Sutcliffe, Geoff , 編. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28 (Cham: Springer International Publishing). 2021: 625–635. ISBN 978-3-030-79876-5. doi:10.1007/978-3-030-79876-5_37 （英語）.
- ^ About. Lean Language. [2024-03-13].
- ^ Significant changes from Lean 3. Lean Manual. [24 March 2023].
- ^ Mission. Lean FRO. 2023-07-25 [2024-03-14].
- ^ std4. GitHub. [2024-03-13].
- ^ Building the Mathematical Library of the Future. Quanta Magazine. （原始內容存檔於2 Oct 2020）.
- ^ Lean community. leanprover-community.github.io. [2023-10-24].
- ^ Mathlib statistics. leanprover-community.github.io. [2024-06-21].
- ^ Installing Lean 4 on Linux. leanprover-community.github.io. [2024-06-21].
- ^ Hales, Thomas. A Review of the Lean Theorem Prover. Jigger Wit. September 18, 2018. （原始內容存檔於21 Nov 2020）.
- ^ Buzzard, Kevin. The Future of Mathematics? (PDF). [2020-10-06].
- ^ Formal Abstracts. Github.
- ^ What is the Xena project?. Xena. 8 May 2019 （英語）.
- ^ Hartnett, Kevin. Proof Assistant Makes Jump to Big-League Math. Quanta Magazine. July 28, 2021. （原始內容存檔於2 Jan 2022）.
- ^ Sloman, Leila. 'A-Team' of Math Proves a Critical Link Between Addition and Sets. Quanta Magazine. 2023-12-06 [2023-12-07] （英語）.
- ^ Solving (some) formal math olympiad problems. OpenAI. February 2, 2022 [March 13, 2024].
- ^ Teaching AI advanced mathematical reasoning. Meta AI. November 3, 2022 [2024-03-13].