3 ms·
> Lean is a new open source theorem prover being developed at Microsoft Research. It is a research project that aims to bridge the gap between interactive and a
by Gys 3y ago
> Lean is a new open source theorem prover being developed at Microsoft Research. It is a research project that aims to bridge the gap between interactive and automated theorem proving. Lean can be also used as a programming language. Actually, some Lean features are implemented in Lean itself.
- karmakaze 3y agoI've heard of Lean some time ago and is now v4. Is the opensource part which is new or has this text not been updated since v1?
- uxp8u61q 3y agoI have trouble parsing your sentence, so hopefully what follows will help. - Lean has always been open source. - Lean 4 has been in development for a while, with the first milestone (alpha version) published in January 2021.