[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