I think that (most) mathematicians were not that interested in formal proof until quite recently (as opposed to computer scientists), and most of the interest in lean has been self-reinforcing, namely there is a (relatively speaking) huge library of formally verified mathematics. So now basically anyone who cares about formal verification as a tool for mathematics is working in lean. There are of course numerous techincal differences which you can read about if you google coq vs lean.