Comment by kevinbuzzard

Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4).

I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".