跳转到内容

用户: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]. 

外部链接