I have at least some level of experience with advanced maths, but the thing that always struck me was how amenable to automation that a lot of it seemed. While it might be creative for a human to come up with the Schreier refinement theorem, for example, I don't think it fundamentally requires creativity.

On some level, I think the most straightforwardly creative work in maths comes from building up useful generalizations; I can't see current LLMs inventing even something as straight forward as a manifold from first principles; but I also don't think that's fundamentally required to prove useful things, I think it's more of a shortcut for humans.