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 <bba...@mit.edu> > > * Package name : lean > Version : 3.2.0 > Upstream Author : Leonardo de Moura <leona...@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