My intuitive understanding is that deriving new theorem from existing concepts is "new math" insofar as it conclusively proves whether existing conjectures are in fact true or not by deriving proofs within an existing formal "system" (loosely understood), but it's not "new math" as it doesn't introduce new concepts to the system. It's the usual problem solver vs. theory builder dichotomy.
An interesting thought experiment would be: assuming AI can solve any given problem (or prove it's undecidable), and thus that the "proving" activity becomes trivialized, what's the interesting part that remains? Can we work on "refactoring" mathematics to make it more intuitive? More "powerful" in some sense? What are other refactorings that are worth exploring?
An interesting thought experiment would be: assuming AI can solve any given problem (or prove it's undecidable), and thus that the "proving" activity becomes trivialized, what's the interesting part that remains? Can we work on "refactoring" mathematics to make it more intuitive? More "powerful" in some sense? What are other refactorings that are worth exploring?