I think the central problem with that line of reasoning is that it supposes we are already living with AGI. Even the latest PR from Anthropic admits that we are not [0] there yet. If we don't have AGI capable of integrating and employing the mathematical results produced by an artificially superintelligent theorem prover so that they become useful to the rest of science and engineering, we will need humans to do at least some of the work in mathematics. Moreover if we freeze current AI capabilities today, "digestion" probably doesn't scale, so mathematical research will probably end up AI-assisted in ways not far off from what we're already seeing in the sciences.
[0] https://www.anthropic.com/research/claude-shaped-science