Oh, PhDs, you're right, that's not approximately no one... It's probably approximately one.

I like Lean (and more generally dependent types) but ffs Lean has a very, very small userbase for a project like this. GGP would have to really justifyv the benefits for such a switch.