I think the biggest hurdle remaining is that all these landmark results are generally counter-examples.

Proving something in the affirmative often requires the creation of an entire new sub-field of math, or new tools. Think of Fermat's Last Theorem or something like that.

These results, while impressive, are clever constructions using existing techniques. It isn't clear that AIs can build new machinery like this. But if/when they can, yeah it is probably game over.