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].