> about what I'd expect pre-generative-AI counterexample search systems to be able to find.

The difference today (and the reason why everyone is excited about it) is that the same system that does advanced math can write poetry, play an above average game of chess, code frontend/backend stuff and do cybersec. These are not "expert systems", nor are they trained for each task individually. That's the catch.

> just indicated that humans had not spent enough time thinking about the problem

Heh, this is a weak excuse. We've seen variations on this theme every time something cool gets solved by the models.