I'm reminded of the joke about the two friends who come across a bear in the woods. When one puts on running shoes, his friend chides him that he can't outrun the bear. He responds, "I don't need to outrun the bear, I just need to outrun you."

AI doesn't have to implement Hilbert's vision and be able to prove everything. I just has to out-prove human mathematicians.