LEAN has significant momentum right now. I was at the International Congress of Mathematical Software this summer (as a plenary speaker), and the other plenary was about LEAN, as were a bunch of talks. There are also excellent VSCode, Emacs, and CoCalc modes for using LEAN. The Zulip LEAN chat channel (https://leanprover.zulipchat.com/) is also very active.