Lean Prover
Lean is a functional programming language and interactive theorem prover based on dependent type theory. Dependent type theory unites the worlds of programs and proofs; thus, Lean is also a programming language.
Cost / License
- Free
- Open Source
Application type
Platforms
- Mac
- Windows
- Linux
- Visual Studio Code
Features
- Ad-free
Tags
- proof-assistant
- vscode-extension
Lean Prover News & Activities
Recent activities
- niksavc liked Lean Prover
- jtsak added Lean Prover
- POX updated Lean Prover
jtsak added Lean Prover as alternative to Rocq Prover, Isabelle and Agda
Lean Prover information
Developed by
Lean Licensing
Open Source (Apache-2.0) and Free product.Alternatives
3 alternatives listedSupported Languages
- English
What is Lean Prover?
Lean is a functional programming language and interactive theorem prover based on dependent type theory. Dependent type theory unites the worlds of programs and proofs; thus, Lean is also a programming language. Lean takes its dual nature seriously, and it is designed to be suitable for use as a general-purpose programming language—Lean is even implemented in itself.
Lean was developed by Microsoft Research in 2013 as an initial effort to help mathematicians and engineers solve complex math problems. Lean is an open-source development environment for formal mathematics, also known as machine-checkable mathematics, used by and contributed to by an active community of mathematicians around the world.