This. Math proofs are useless in 99.99% of situations because they are far too expensive to actually use in production. Only something like AWS would use formal proofs to verify some system property for reliability.

With some super-math Q* bot, a mathematician could presumably create actual proofs/simplifications for complex real world problems/systems at very affordable time and costs (in weeks not years).

The mathematician in this case is far less skilled than the bot, but that doesn't detract from their market value. Most programmers are way less skilled/smart than the library authors that they rely on, that doesn't stop them from earning $$$, because they are useful.