lean

interactive and automated theorem prover

WWW CVSWeb GITHub
  1. Package version
    lean-3.48.0
  2. Maintainer
    Theo Buehler

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.

  • devel/cmake
  • devel/ninja
  • lang/python/3.10