With Fermat's theorem, the genius was in the original theorem. Which then caused generations of mathematicians to break their heads over trying to prove it correct. Fermat didn't write down a proof. His theorem was famously just a scribble in a side line of a book. Probably it was something that he had an hunch about that he couldn't quickly falsify.
I don't think AI is being used much for coming up with new problems yet. But I don't see why that would not be possible either. It's the obvious next frontier after AI clears the backlog of existing theorems. I imagine scientists are already using AI to find new interesting problems to work on and generally explore the problem space. But fundamentally, the reflex of asking or imagining "if this is true, what else could be true" is something that distinguishes people from AIs. For now at least.