Useful mathematics need not mean understandable by humans. Why cannot AI, in the future, also figure what mathematics is useful. Whatever role we see for humans in mathematics, could possibly be picked up (and done better) by AI (in the future). Choosing proofs, strategies, abstractions, figuring utility, intuitiveness, all are in principle a search problem, including meta-search where needed.

I wonder if the advantage AI has is simply that it has absorbed vastly more collective mathematical experience and can therefore provide better search heuristics than a human.