Hi Benjamin, please consider the option of maintaining this package under the roof of the Debian Science Team.
Best regards Anton Am Mittwoch, 28. Juni 2017 schrieb Benjamin Barenblat : > Package: wnpp > Severity: wishlist > Owner: Benjamin Barenblat <bba...@mit.edu <javascript:;>> > > * Package name : lean > Version : 3.2.0 > Upstream Author : Leonardo de Moura <leona...@microsoft.com > <javascript:;>> 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. > -- Anton
