[ViscountPenguin]

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.

[gmadsen]

Sure in the same way you could automate Shakespeare plays by having a room full of monkeys with typewriters.

The space of mathematical statements is infinite. Having the taste, insight, and creativity to reach points in that space that are meaningful to humans is the entire game