Ranked in these QuestionsQuestion Ranking
Pro Interactive tutorial runs in the browser
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