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.