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

[Andreas Tille <andreas@an3as.eu>]

Hi Benjamin,

Thanks for this ITP.
I'd suggest to package this in Debian Science team.

Kind regards

     Andreas.

On Wed, Jun 28, 2017 at 05:37:53PM -0400, Benjamin Barenblat wrote:
> 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.

-- 
http://fam-tille.de