[HeavyStorm]

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.

[jcelerier]

Apparently roughly ~150k math PhDs live on earth right now, assuming they all know Lean that's between 0.001% and 0.002% of earth population so quite closer to no one than one