It would be nice if one of these models would produce a novel theory or advance the field in a positive direction.
Most (all?) of the big discoveries have been counterexamples, which is just sort of a systematic tearing down human ingenuity. I know that counterexamples are an important part of progress and discovery, but it just feels bad to me.
But I'm not a mathematician, maybe I'm totally misreading the vibe.
this isn't really true anymore. First, a number of the big results are constructions, not counterexamples. For example the existence of a non-sofic group. It was widely believed that non-sofic groups existed (so it wasn't a "counterexample" to a widely believed conjecture), but no constructions were known.
There are other examples though. For example, NP hardness of n^{1/400}-approx CVP. Like any NP hardness proof, this shows you can faithfully encode a hard problem (3SAT here iirc) in terms of another candidate hard problem. Not really a counterexample at all.
Not all, see the cycle double cover conjecture proof: https://news.ycombinator.com/item?id=48863490
But yeah, Terry Tao considered this exact situation in advance and is on record that this exact outcome (rushing to priority before an explanation) would be the worst possible result. https://mathstodon.xyz/@tao/117207849921390904
We will have to see whether any other millennium problems fall. I guess that in a year the scope of AI math will be much clearer, for now it's still a bunch of incidents of unclear pattern.