Comment by kdavis

Looking a bit more into this, it doesn't seem your claim "most of the consequences of additional axioms have been worked out" holds up.

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.