Coq and Isabelle are much more mature systems, they have already been used in a lot of big developments, and they have large user communities and existing textbooks and so on.

Agda is pretty finicky, proving stuff in it is harder and the entire project feels more researchy (as a playground to try out ideas for programming languages).

Lean seems promising, but it's still kind of new, so compared to Coq will not find as much documentation, and there are fewer people on Stack Overflow to answer questions.