I guess you can see this as an exploration problem, in pure maths, while the goal is to solve a conjecture, the limitation of humans on pure computational power led to the exploration of alternative paths. Sometimes, these paths weren't leading to solving the initial conjecture but opened new idea and new direction. Sometimes a less direct but more humanly natural path was taken to solve the conjecture which also led to new and humanly understandable questions. In some ways solving the question wasn't the most important part of the work, as this doesn't have direct impact on our life (as I saw people comparing this with drug discovery), but the path leading to the solution raised new conjectures and techniques that further developed the field.

I have a really hard time reading AI proof so this might be a biased statement, but most of them feels like having a superpowerfull machine, that would have bruteforce all the possible words of finite length in your logical syntax. You have the path to the solution, using tools that where already known and even direction that where abandoned because they seemed to fail for our human brain. But at the end, as a mathematician, you don't learn anything that is really new.

To me this is the main risk with AI and in general the one most mathematican try to explain but fail, we might miss a lot of alternative path that would have raised more interesting questions (I think this is already more or less what is happening). On top of that, we will run out of mathematicians as no one wants to pursue a career in the field anymore.