I'm not a mathematician but AFAICT AI in mathematics only helped for paradigmatic works, either verification of well explained, and even researched, conjectures. Ideas that have been labelled as potentially interesting, are verifiable, and in a well known area. It is already quite useful... but it is NOT about paradigm change. It's not about revolutionary ideas. It's about being able to slightly more efficiently do more of of the same.

It is precisely NOT about big questions but rather potentially covering and thus cornering away all the "small" questions.

PS: already argued for something similar in recent Ergos related work, see comment history.