Reminds me of the idea of Radical Monopolies from Ivan Illich in a way. If a technology or service becomes so wide spread within society, even though many different versions of the technology or service may exist, a Radical Monopoly means that non users will suffer for their non use. Cars and non drivers in cities are the typical example. And I wonder, whether mathematicians who don't user theorem provers will soon suffer under the tyranny of the theorem provers, whether it be Lean or one of the others.

▲

eru 2 hours ago | parent [-]

> Cars and non drivers in cities are the typical example.

Have a look at Dutch cities for how to avoid this.

▲

data-ottawa 2 hours ago | parent [-]

I immediately thought that’s not totally fair due to the size of the Netherlands vs other countries.

I asked Mistral to do an analysis: nearly zero R^2 for car ownership vs log country area, and it’s the same with proportion of urban population in OECD countries.

Netherlands isn’t very different from peers in car ownership, they just treat cyclists very well it seems.

This is a total tangent, just found it interesting.

▲

applfanboysbgon an hour ago | parent [-]

As it turns out, people live in cities[1]. The amount of empty space a country has outside of cities doesn't have much bearing on navigation and infrastructure inside cities.

[1] https://xkcd.com/1138/

	▲	data-ottawa 43 minutes ago \| parent [-]
		Right, but there’s zero correlation between urban population percentage and cars per capita either, which was surprising to me. I’d have expected a vague logistic curve.