[firesteelrain]

I believe this is what we wanted computers to help us solve along with other prior hard problems prior to computers. This should be viewed as a good thing even if Anthropic, OpenAI, etc benefit just like IBM benefitted from mainframes.

[fidotron]

Indeed. I specifically recall my logic lecturers in a compsci course expressing the view the one purpose of computers is to work towards enabling automatic proofs, partly because they saw this as the universal problem in compsci (esp compilers) as well as massive potential for scientific progress generally.