There's a substantial gap between "the machine is better than human mathematicians" and "the machine can formalize a solution to any problem immediately." Much of the important mathematical theory behind modern science was mapped out in advance by mathematicians, and scientists were able to find and take advantage of this mathematics where applicable. Mapping out our understanding of e.g. physics and our understanding of mathematics in parallel and finding connections later has historically been a highly successful approach, and I see no reason to believe the same would not be true for advanced machines. Would Einstein have been able to formulate GR without the existing theory of differential geometry? Maybe, but maybe not. Would an advanced machine be able to develop the theory of differential geometry in response to gravitational measurements? Maybe, but maybe not.

Edit: Perhaps I could have been terser here. Really the idea is that small jumps are easier to make than big jumps. Continually developing pure mathematics is a way to make small jumps in logic and intuition add up to big jumps in applications.

> A real-world system with the abilities of a robustly superintelligent mathematician can, when some practical problem requires it, formulate a problem statement, churn for a bit, spit out a formalized answer, and continue whatever outer-loop task it was doing without a human even finding out.

Without anyone ever finding out.

In the long run this means almost no progress past what we already have, because there's no shoulders of giants to stand on. Not even AI shoulders.

There are some parallels here to AI coding where even if the AI can write all the code, it's still valuable to have a human who can read and understand the code to verify correctness. The same is true of AI generated math proofs that humans will want to verify are around before they feed them back into the AI and build new insights.