In many ways, the teleporting machine that teleports to the solution is against the point of the questions. No one wants the solution to be "Run $10,000,000 worth of tokens to cover all possible Lean formulations of the problem".
I think for Mathematicians, I'd say that the human level formulation is still possible and with a new perspective. We as a society (and outside of Mathematics) need to also understand that this AI teleport to the answer thing has less value than we all expected. The value is in the journey.
The open question is if people will still want to take the journey if the teleport machine exists. Or if the existence of the teleport machine halts exploration.
You're overlooking that the teleport machine costs lots of money to use. The AI providers are not going to waste money by teleporting randomly around.
Someone is going to have to find a new destination that is worth spending the money to teleport to (or walk by themselves) and that someone is mathematicians.
Meanwhile, the AI labs are doing that for just marketing.
You realize that they don't want that, correct?