His issue is more nuanced than that. Most of the value was in humans reaching new insights or new math during failed attempts to solve these problems, whereas AI is basically "too efficient" in beelining to the goal and discards potential new insights reached along the way. I assume this is solvable.
Surely it is. Ask it to keep a list of all the promising sub paths, reprompt the collections of agents again on these after the main problem has been addressed. Or even release a list of them and let others investigate.
Well, if in future we do end up with a magical tool that can solve any formal mathematical problem on a whim, we really won’t need field of mathematics anymore as it is today.
There would be no need to deliver new mathematical insights by solving problems. You would just have a magical math problem solving machine and that’s it.