This is really well written and exposes a core tension between science and something akin to engineering. The "engineering" of proofs has become "easy" (a compute and $) problem, rather than hard (a time and conception problem).

Without the ability to do things the "hard" way it is difficult to figure out if doing things the "easy" way will help us advance the frontier of math and science.

I may be wrong but historically we had this version of science discovery for a long while (empirical observation and brute force application) rather than first principles leading to applications (tools, the wheel, mills etc). Then somewhere along the way it flipped after Newton and the enlightenment period and started understanding first principles before they become engineering applications.

Perhaps it is not required, and we can just keep doing things the "easy" way like we used to, or we might find ourselves out of the ability to brute force things and then we go back to needing to do this the hard way, at which point this period of AI brute forcing would be seen as a detriment.