Lean (proof assistant): Difference between revisions

From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
No edit summary
Add information on Lean 4
Line 30: Line 30:


Started in 2017, the user-maintained library ''mathlib'' contains the largest collection of mathematics that has been formalized in Lean. As of February 2023, mathlib contains over 100,000 theorems and 1,000,000 lines of code.<ref>{{Cite web |title=Mathlib statistics |url=https://leanprover-community.github.io/mathlib_stats.html |access-date=2023-02-12 |website=leanprover-community.github.io}}</ref>
Started in 2017, the user-maintained library ''mathlib'' contains the largest collection of mathematics that has been formalized in Lean. As of February 2023, mathlib contains over 100,000 theorems and 1,000,000 lines of code.<ref>{{Cite web |title=Mathlib statistics |url=https://leanprover-community.github.io/mathlib_stats.html |access-date=2023-02-12 |website=leanprover-community.github.io}}</ref>

In prior releases of Lean, several core parts of the system's logic were not amenable to being modified. A user wishing to change these parts of the system would need to modify the C++ implementation of Lean. Furthermore, overhead associated with [[Virtual_machine#Process_virtual_machines|virtual machine]] interpretation meant that the efficiency of Lean was not competitive with other proof assistants such as [[Coq]]. In 2021, Leonardo de Moura and Sebastian Ullrich released Lean 4: a reimplementation of the Lean theorem prover within itself, with the aim of addressing the two aforementioned criticisms. Lean 4 produces [[C (programming language)|C]] code which is then compiled, enabling the development of efficient domain-specific automation.<ref>{{cite book |last1=Moura |first1=Leonardo de |last2=Ullrich |first2=Sebastian |editor1-last=Platzer |editor1-first=Andr'e |editor2-last=Sutcliffe |editor2-first=Geoff |title=Automated Deduction -- CADE 28 |date=2021 |publisher=Springer International Publishing |isbn=978-3-030-79876-5 |pages=625-635 |url=https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37#citeas |access-date=24 March 2023}}</ref> Lean 4 is not [[Backward compatibility|backwards-compatible]] with Lean 3.<ref>{{cite web |title=Significant changes from Lean 3 |url=https://leanprover.github.io/lean4/doc/lean3changes.html |website=Lean Manual |access-date=24 March 2023}}</ref>


Lean has gotten attention from mathematicians [[Thomas Callister Hales|Thomas Hales]]<ref name="Hales" /> and [[Kevin Buzzard]].<ref name="Buzzard" /> Hales is using it for his project, Formal Abstracts.<ref>{{cite web |title=Formal Abstracts |url=https://formalabstracts.github.io/ |website=Github}}</ref> Buzzard uses it for the Xena project.<ref>{{cite web |title=What is the Xena project? |url=https://xenaproject.wordpress.com/what-is-the-xena-project/ |website=Xena |language=en |date=8 May 2019}}</ref> 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.
Lean has gotten attention from mathematicians [[Thomas Callister Hales|Thomas Hales]]<ref name="Hales" /> and [[Kevin Buzzard]].<ref name="Buzzard" /> Hales is using it for his project, Formal Abstracts.<ref>{{cite web |title=Formal Abstracts |url=https://formalabstracts.github.io/ |website=Github}}</ref> Buzzard uses it for the Xena project.<ref>{{cite web |title=What is the Xena project? |url=https://xenaproject.wordpress.com/what-is-the-xena-project/ |website=Xena |language=en |date=8 May 2019}}</ref> 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.

Revision as of 12:44, 24 March 2023

Lean
ParadigmFunctional programming, Imperative programming
DeveloperMicrosoft Research
First appeared2013; 11 years ago (2013)
Stable release
3.48.0 / 17 September 2022; 19 months ago (2022-09-17)
Preview release
4.0.0-m5 / 7 August 2022; 21 months ago (2022-08-07)
Typing disciplineStatic, strong, inferred
Implementation languageC++, Lean
OSCross-platform
LicenseApache License 2.0
WebsiteStable: leanprover-community.github.io
Preview: leanprover.github.io
Influenced by
ML
Coq
Haskell

Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types.

The Lean project is an open-source project hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013.[1]

Lean has an interface, implemented as a Visual Studio Code extension and Language Server Protocol server, that differentiates it from other interactive theorem provers. 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.

Started in 2017, the user-maintained library mathlib contains the largest collection of mathematics that has been formalized in Lean. As of February 2023, mathlib contains over 100,000 theorems and 1,000,000 lines of code.[2]

In prior releases of Lean, several core parts of the system's logic were not amenable to being modified. A user wishing to change these parts of the system would need to modify the C++ implementation of Lean. Furthermore, overhead associated with virtual machine interpretation meant that the efficiency of Lean was not competitive with other proof assistants such as Coq. In 2021, Leonardo de Moura and Sebastian Ullrich released Lean 4: a reimplementation of the Lean theorem prover within itself, with the aim of addressing the two aforementioned criticisms. Lean 4 produces C code which is then compiled, enabling the development of efficient domain-specific automation.[3] Lean 4 is not backwards-compatible with Lean 3.[4]

Lean has gotten attention from mathematicians Thomas Hales[5] and Kevin Buzzard.[6] Hales is using it for his project, Formal Abstracts.[7] Buzzard uses it for the Xena project.[8] 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.

Examples (Lean 3)

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. 

definition add : nat → nat → nat
| n zero     := n
| n (succ m) := succ (add n m)

This is a simple proof in lean in term mode. 

theorem and_swap : p ∧ q → q ∧ p :=
    assume h1 : p ∧ q,
    ⟨h1.right, h1.left⟩

This same proof can be accomplished using tactics. 

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
begin
    assume h : (p ∧ q), -- assume p ∧ q is true
    cases h, -- extract the individual propositions from the conjunction
    split, -- split the goal conjunction into two cases: prove p and prove q separately
    repeat { assumption }
end

See also

References

  1. ^ "Lean Prover About Page".
  2. ^ "Mathlib statistics". leanprover-community.github.io. Retrieved 2023-02-12.
  3. ^ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff (eds.). Automated Deduction -- CADE 28. Springer International Publishing. pp. 625–635. ISBN 978-3-030-79876-5. Retrieved 24 March 2023.
  4. ^ "Significant changes from Lean 3". Lean Manual. Retrieved 24 March 2023.
  5. ^ Hales, Thomas (18 September 2018). "A Review of the Lean Theorem Prover". Retrieved 6 October 2020.
  6. ^ Buzzard, Kevin. "The Future of Mathematics?" (PDF). Retrieved 6 October 2020.
  7. ^ "Formal Abstracts". Github.
  8. ^ "What is the Xena project?". Xena. 8 May 2019.

External links

Retrieved from "https://en.wikipedia.org/w/index.php?title=Lean_(proof_assistant)&oldid=1146365928"