Your model of what AI is good at is wrong. Generative AI is not good at wandering off into novel esoteric abstract corners while maintaining correctness, it is good at things that are close to its training data. I suspect that humans will long outperform AI in the domain of "novel esoteric abstract useless math" whereas AI will outperform humans in the domains of (1) making connections between already-well-understood concepts, things that seem obvious in retrospect but which no human figured out just because of the accidents of what people happened to focus on, and (2) proving things that require long, tedious, intellectually unsatisfying calculations, which would cause a human mathematician to give up for boredom.

My understanding is that we’re talking about “tool-assisted” proof generation, which provides some guard rails but would still allow significant creativity. Tools like Lean, Coq, etc.