Lean (proof assistant)

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

Lean (proof assistant)
Developer(s)Microsoft Research
Initial release2013 (2013)
Stable release
3.4.2 / 18 January 2019 (2019-01-18)
Repositorygithub.com/leanprover/lean
Written inC++
Operating systemCross-platform
Available inEnglish
TypeProof assistant
LicenseApache License 2.0
Websiteleanprover.github.io

Lean has a number of features that differentiate it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols. (These can be typed using LaTeX-like sequences, such as "\times" for "×".) Lean uses its own language for meta-programming. So, if the user wants to write a function that automatically proves some theorems, they write that function in Lean's own language.

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

Here is how the natural numbers are defined in Lean.

inductive nat : Type
| zero : nat
| succ : nat → nat

Here is the addition operation defined for natural numbers.

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

This is a simple proof in learn 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
gollark: ΠοτατΟΣ Ταυ
gollark: ʽʽʽʽʽʽʽʽʽʽ
gollark: ἁτ;
gollark: 🌵
gollark: Well, if you claim it, I'll add it to my list of "places to make XP farms from".

See also

References
  1. Hales, Thomas. "A Review of the Lean Theorem Prover". Retrieved 21 January 2020.
  2. Buzzard, Kevin. "The Future of Mathematics?" (PDF). Retrieved 21 January 2020.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.