Comment by Ohentis

Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).