17 lines
587 B
Plaintext
17 lines
587 B
Plaintext
{{language
|
|
|exec=machine
|
|
|strength=strong
|
|
|safety=safe
|
|
|checking=both
|
|
|gc=yes
|
|
|LCT=yes}}
|
|
{{implementation|Lean}}
|
|
{{language programming paradigm|functional}}
|
|
{{language programming paradigm|dependent-types}}
|
|
|
|
|
|
'''Lean''' is an open source theorem prover and programming language being developed at Microsoft Research.
|
|
|
|
Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.
|
|
|
|
https://leanprover.github.io/about/ |