The people who could instruct such AI and evaluate its outputs would be domain experts. Without them how would you even start to approach those problems?
I think we'll see something analogous to the classification of the finite simple groups collaboration, but where some core researchers will do several proofs in the area to show it the kinds of things needed and it can help fill in others. Things where there is a large volume of similar work to be done.