And then there's all the math problems if solved where the information is new to every human on earth.

This is not novel. Computers have been generating mathematical information that would be resource-prohibitive to produce by hand since the dawn of computing.

The ingenious aspect seems to be that we've found simpler ways to apply computing power to a broader range of problems, which it's important to note is as much a testament to the developers of proof assistants like Lean as it is to LLM developers, to say nothing of the countless mathematicians over many centuries that contributed training data.

Whether this will lead to many revolutions, or a handful of impressive results followed by a long dark spell remains to be seen.

I, for one, wouldn't place large bets on either.