Re: Bug#866334: ITP: lean -- theorem prover from Microsoft Research
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
Reply to: