> Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and auto

> Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving. https://leanprover.github.io/papers/system.pdf https://leanprover.github.io/papers/system.pdf - "The Lean Theorem Prover." Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer, 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015. https://leanprover-community.github.io/index.html https://leanprover-community.github.io/index.html - Lean community