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?

You could regard existing mathematical techniques as a set of Lego pieces. If you build a proof just using those pre-existing Lego pieces then it may be a new proof (a new Lego model), but it's not a new Lego piece - a new piece of mathematical machinery.