I think two primary things, which are connected. First, Kevin Buzzard, a “real” mathematician (as he self-identifies), promoted computer formalization of research mathematics with the Xena project, and second when looking for tools he latched onto Lean because he felt it more ergonomic. [1]

He later discovered why Coq, Isabelle/HOL, and other tools did things in certain ways [2] (which were more “natural” to computer scientists) but by then his advocacy and inertia (the growing, curated MathLib) cemented Lean as the tool mathematicians tried first and sort of stuck with.

[1] https://news.ycombinator.com/item?id=21200721

[2] https://xenaproject.wordpress.com/2020/07/03/equality-specif...