Comment by QuesnayJr
5 hours ago
I'm sure AI could contribute to this, but this is already a well-developed field of mathematics, and most of the consequences of additional axioms have been worked out. (The most productive hypothesis has been what's called "projective determinacy", if you're curious.)
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".
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 additional axioms have been worked out as each new set of axioms means re-deriving (similar?) results 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.
What name does this "well-developed field of mathematics" go by? (I just want to get a taste of what the field is like.)
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".