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?
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".
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".