All of these breakthroughs are in verifiable brute force domains, and some of them are probably wrong because of a typo in a lean specification or just a base level axiom being incomplete.

I think the better the way to think about LLMs is like they are new substances, like when we first discovered clay or bronze, but confined to the digital realm. Previously we were chipping away at stones trying to make to things as close to useful as possible, then we found a step change. LLMs are like clay but they have their limitations. Wake me up when they are proposing new, { conjecture: interesting|useful|new } and not as a side effect of trying to get to a goal.