Lean is a
theorem prover and
programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
. It is based on the
calculus of constructions with
inductive type
In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a ...
s.
The Lean project is an open source project, hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013.
Lean has an interface that differentiates 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
Latex is an emulsion (stable dispersion) of polymer microparticles in water. Latexes are found in nature, but synthetic latexes are common as well.
In nature, latex is found as a milky fluid found in 10% of all flowering plants (angiosperms ...
-like sequences, such as "\times" for "×".) Lean also has an extensive support for meta-programming.
Lean has gotten attention from mathematicians
Thomas Hales and
Kevin Buzzard
Kevin Mark Buzzard (born 21 September 1968) is a British mathematician and currently a professor of pure mathematics at Imperial College London. He specialises in arithmetic geometry and the Langlands program.
Biography
While attending the Roy ...
.
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
Imperial College London (legally Imperial College of Science, Technology and Medicine) is a public research university in London, United Kingdom. Its history began with Prince Albert, consort of Queen Victoria, who developed his vision for a cu ...
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 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
end
See also
*
Dependent type
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifier ...
*
List of proof assistants
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
*
mimalloc
mimalloc (pronounced "me-malloc") is a free and open-source compact general-purpose memory allocator developed by Microsoft with focus on performance characteristics. The library is about 11000 lines of code and works as a drop-in replacement for ...
*
Type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
References
External links
Lean WebsiteLean Community WebsiteThe Natural Number Game- An interactive tutorial to learn lean
{{Microsoft Research
Programming languages created in 2013
Proof assistants
Dependently typed languages
Educational math software
Functional languages
Free and open-source software
Free software programmed in C++
Microsoft free software
Microsoft programming languages
Microsoft Research
Software using the Apache license