That overhang seems like a precious resource for AI companies. They can exploit that overhang to inflate the impression of AI's capabilities, and hopefully that exploitation will discourage the next generation of mathematicians from pursuing math. If they play their cards right, OpenAI and Anthropic can dominate the field even if they ultimately can't replicate the creativity of human mathematicians, because they'll have driven their competition out.
What we should be trying to achieve is a ladder-breaking maneuver: knock out the lower rungs so no person can reasonably climb to the top-reaches of mathematical skill anymore. That may ultimately result in stagnation, but it's what's best for AI, so it's what should be done now.
We need to do everything we can to create the greatest-possible dependence on AI tools.