interactive and automated theorem prover
Lean is an open source theorem prover and programming language. It 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.
Homepage: https://leanprover-community.github.io
Maintainer: Theo Buehler <tb@openbsd.org>