Bug#866334: ITP: lean -- theorem prover from Microsoft Research

[Benjamin Barenblat <bbaren@mit.edu>]

Package: wnpp
Severity: wishlist
Owner: Benjamin Barenblat <bbaren@mit.edu>

* Package name    : lean
  Version         : 3.2.0
  Upstream Author : Leonardo de Moura <leonardo@microsoft.com> et al.
* URL             : https://leanprover.github.io/
* License         : Apache-2.0
  Programming Lang: C++
  Description     : theorem prover from Microsoft Research

Lean is a theorem prover or interactive proof assistant. That is, it’s
a system in which you can write formal mathematical proofs that are
checked for correctness by the computer. Lean is thus broadly similar
to Coq, but the Lean developers hope to build a faster, more extensible
system than Coq is today.

From the About page: “Lean is a new open source theorem prover being
developed at Microsoft Research, and its standard library at Carnegie
Mellon University. 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. The goal is to support both mathematical
reasoning and reasoning about complex systems, and to verify claims in
both domains.”

Lean has been under development for several years; regular releases
first appeared in January. I use Lean, and I know other Debian users
would like to have it easily accessible.