Lean (proof assistant)
 | |
| Paradigm | Functional programming, Imperative programming |
|---|---|
| Developer | Lean Focused Research Organization (FRO) |
| First appeared | 2013 |
| Stable release | 4.3.0
/ 30 November 2023 |
| Preview release | v4.4.0-rc1
/ 30 November 2023 |
| Typing discipline | Static, strong, inferred |
| Implementation language | Lean , C++ |
| OS | Cross-platform |
| License | Apache License 2.0 |
| Website | lean-lang |
| Influenced by | |
| ML Coq Haskell | |
Lean is a proof assistant and programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. It was principally developed by Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services, and has had significant contributions from other coauthors and collaborators during its history.
History
Initially launched by Leonardo de Moura at Microsoft Research in 2013.[1] The initial versions of Lean, later known as Lean 1 and 2, were experimental and contained features such as support for Homotopy Type Theory based foundations that were later dropped.
Lean 3 (first released Jan 20, 2017) was the first moderately stable version of Lean. It was implemented primarily in C++ with some features written in Lean itself. After version 3.4.2 Lean 3 was officially end-of-lifed while development of Lean 4 began. In this interim period members of the Lean community developed and released unofficial versions up to 3.51.1.
In 2021, Lean 4 was released which was a reimplementation of the Lean theorem prover capable of producing C code which is then compiled, enabling the development of efficient domain-specific automation.[2] Lean 4 also contains a macro system and improved typeclass synthesis and memory management procedures over the previous version. Another benefit compared to Lean 3 is the ability to avoid touching C++ code in order to modify the frontend and other key parts of the core system, as they are now all implemented in Lean and available to the end user to be overridden as needed.[citation needed]
Lean 4 is not backwards-compatible with Lean 3.[3]
Overview
Libraries
In 2017, a community-maintained project to develop a Lean library mathlib began, with the goal to digitize as much of pure mathematics as possible in one large cohesive library, up to research level mathematics.[4][5] As of November 2023, mathlib had formalized over 127,000 theorems and 70,000 definitions in Lean.[6]
Editors integration
Lean integrates with:[7]
- Visual Studio Code
- Neovim
- Emacs
Interfacing is done via a client-extension and Language Server Protocol server.
It has native support for Unicode symbols, which can be typed using LaTeX-like sequences, such as "\times" for "×". Lean can also be compiled to JavaScript and accessed in a web browser and has extensive support for meta-programming.
Examples (Lean 4)
The natural numbers can be defined as an inductive type. This definition is based on the Peano axioms and states that every natural number is either zero or the successor of some other natural number.
inductive Nat : Type | zero : Nat | succ : Nat → Nat
Addition of natural numbers can be defined recursively, using pattern matching.
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)
This is a simple proof in Lean using tactic mode:
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by intro h -- assume p ∧ q with proof h, the goal is q ∧ p apply And.intro -- the goal is split into two subgoals, one is q and the other is p · exact h.right -- the first subgoal is exactly the right part of h : p ∧ q · exact h.left -- the second subgoal is exactly the left part of h : p ∧ q
This same proof in term mode:
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
fun ⟨hp, hq⟩ => ⟨hq, hp⟩
Usage
Lean has gotten attention from mathematicians Thomas Hales[8] and Kevin Buzzard.[9] Hales is using it for his project, Formal Abstracts.[10] Buzzard uses it for the Xena project.[11] One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean.
In 2021, Lean was used to formalize a new proof by Peter Scholze in the area of condensed mathematics,[12] and so as in 2023 by Terence Tao on formalizing proof of Polynomial Freiman-Ruzsa (PFR) conjecture, proving that Lean can be useful at the cutting edge of mathematical research.[13]
See also
- Dependent type
- List of proof assistants
- mimalloc
- Type theory
- Focused Research Organization
References
- ↑ "Lean Prover About Page". https://leanprover.github.io/about/.
- ↑ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff. eds. Automated Deduction -- CADE 28. Springer International Publishing. pp. 625–635. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5. https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37. Retrieved 24 March 2023.
- ↑ "Significant changes from Lean 3". https://leanprover.github.io/lean4/doc/lean3changes.html.
- ↑ "Building the Mathematical Library of the Future". https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/.
- ↑ "Lean community". https://leanprover-community.github.io/lean3/.
- ↑ "Mathlib statistics". https://leanprover-community.github.io/mathlib_stats.html.
- ↑ "Installing Lean 4 on Linux". https://leanprover-community.github.io/install/linux.html.
- ↑ Hales, Thomas (September 18, 2018). "A Review of the Lean Theorem Prover". https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/.
- ↑ Buzzard, Kevin. "The Future of Mathematics?". https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf.
- ↑ "Formal Abstracts". https://formalabstracts.github.io/.
- ↑ "What is the Xena project?" (in en). 8 May 2019. https://xenaproject.wordpress.com/what-is-the-xena-project/.
- ↑ Hartnett, Kevin (July 28, 2021). "Proof Assistant Makes Jump to Big-League Math". Quanta Magazine. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/.
- ↑ Sloman, Leila (2023-12-06). "'A-Team' of Math Proves a Critical Link Between Addition and Sets" (in en). https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/.
External links
- Lean Website
- Lean Community Website
- Lean FRO
- The Natural Number Game- An interactive tutorial to learn lean
 |  |
