使用者:Yinweichen/Testpage1

Lean
編程範型函數式指令式
實作者Lean FRO
面市時間2013年,​11年前​(2013
型態系統靜態、強型推論
實作語言Lean , C++
操作系統跨平台
許可證Apache License 2.0
網站lean-lang.org
啟發語言
ML
Coq
Haskell

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

歷史

編輯

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

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

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

概論

編輯

函式庫

編輯

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

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

編輯器整合

編輯

Lean支援與以下編輯器整合使用:[9]

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

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

人工智能

編輯

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

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

參見

編輯

參考資料

編輯
  1. ^ 1.0 1.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 (英語). 
  2. ^ About. Lean Language. [2024-03-13]. 
  3. ^ Significant changes from Lean 3. Lean Manual. [24 March 2023]. 
  4. ^ Mission. Lean FRO. 2023-07-25 [2024-03-14]. 
  5. ^ std4. GitHub. [2024-03-13]. 
  6. ^ Building the Mathematical Library of the Future. Quanta Magazine. (原始內容存檔於2 Oct 2020). 
  7. ^ Lean community. leanprover-community.github.io. [2023-10-24]. 
  8. ^ Mathlib statistics. leanprover-community.github.io. [2024-06-21]. 
  9. ^ Installing Lean 4 on Linux. leanprover-community.github.io. [2024-06-21]. 
  10. ^ Hales, Thomas. A Review of the Lean Theorem Prover. Jigger Wit. September 18, 2018. (原始內容存檔於21 Nov 2020). 
  11. ^ Buzzard, Kevin. The Future of Mathematics? (PDF). [2020-10-06]. 
  12. ^ Formal Abstracts. Github. 
  13. ^ What is the Xena project?. Xena. 8 May 2019 (英語). 
  14. ^ Hartnett, Kevin. Proof Assistant Makes Jump to Big-League Math. Quanta Magazine. July 28, 2021. (原始內容存檔於2 Jan 2022). 
  15. ^ Sloman, Leila. 'A-Team' of Math Proves a Critical Link Between Addition and Sets. Quanta Magazine. 2023-12-06 [2023-12-07] (英語). 
  16. ^ Solving (some) formal math olympiad problems. OpenAI. February 2, 2022 [March 13, 2024]. 
  17. ^ Teaching AI advanced mathematical reasoning. Meta AI. November 3, 2022 [2024-03-13]. 

外部連結

編輯