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
I am stating a counter-argument to a common argument.
You are simply giving a different argument than the one I'm giving a counter to. Yes, of course, if including human understanding results in strictly better results than AI, then there is an argument for the value supplied by human mathematicians.
But that's an argument that human understanding is on the path to better outcomes. It's not an argument that the intrinsic worth of human understanding is a reason to support mathematicians.