Most of these questions Mathematicians posed to each other have no practical application, and probably will never have a practical application. (ex: the solution to the Navier Stokes question doesn't change anything at all.)

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.