When comparing Coq vs LEAN, the Slant community recommends LEAN for most people. In the question“What are the best dependently typed languages?” LEAN is ranked 4th while Coq is ranked 5th. The most important reason people chose LEAN is:
Lean has a JavaScript version you can try online. (And a faster C++ version you can download.)
Ranked in these QuestionsQuestion Ranking
Pros
Pro Interactive tutorial runs in the browser
Lean has a JavaScript version you can try online. (And a faster C++ version you can download.)
Pro Visual Studio Code support
Lean is a Microsoft Research project, so they have their own IDE support.
Pro Emacs support
Pro Metaprogramming occurs in the same language as the theorem proving.
Because the metaprogramming occurs in the same level as the programming, you are able to write automated tactics that depend on mathematical objects you have already defined, and use those tactics to define more objects. It is a very powerful leap forward in automated and interactive theorem proving.
Pro Permissive license
Apache 2.0