Maybe in the future mathematicians could be the ones proposing different axiomatic foundations (e.g. ZF vs ZF + C vs ZF + C + CH vs ...) and then using computers to examine the consequences of these differing foundations?
Mathematicians have also gone in the opposite direction, and tried to work out what are the weakest foundations where different results hold. This is called "reverse mathematics".
I also thought that there are an infinite set of possible extra axioms, e.g. axiomize any statement that's true but not provably so via Gödel's First Incompleteness Theorem, though maybe the vast majority of such axioms are "uninteresting".
It's true that there's an infinite possible set of axioms. It does seem that the types of axioms that have consequences that humans are interested in fall into simple families. For example, many seemingly unrelated questions are settled by assume the existence of very large sets (larger than can normally constructed in set theory).
Yes, metamathematics is well-developed, but I don't think that most of the consequences of any particular additional set of axioms have been worked out. Each such new set requires re-deriving all of this alternate mathematics from scratch. This is a lot of work!
So I think my original claim---mathematicians select interesting axioms and AI figures out their implications---still seems a possible way forward.
PS: I'd guess descriptive set theory under determinacy is the one place where projective determinacy, as you stated, pays off.
In another direction, there's even a literature on what happens when you allow sets to contain themselves as members, like Aczel's Anti-Foundation Axiom. There's literatures on purely constructive versions of set theory, where everything has to be computable. Like I mentioned before (reverse mathematics), there's work on what happens when you adopt much weaker axiom sets, like second-order arithmetic but weak choice principles such as taking Kruskal's tree theorem as an axiom.
So while AI would accelerate this work, the existing body of work on alternate axioms is tremendous. A surprisingly large amount of it translates between systems, and there are precise tools to measure how weak or strong a system is, relative to its competitors.