However, in most of the experimental sciences, formal results are not the main bottleneck, so speed-ups would be more dependent on progress on coding, fuzzier tasks, robotics, and so on
One difficulty with predicting the impact of “solving math” on the world is the Jevons effect (or a kind of generalization of it). If posing a problem formally becomes equivalent to solving it, it would have effects beyond just speeding up existing fully formal endeavors. It might potentially create qualitatively new industries/approaches relying on cranking out such solutions by the dozens.
E. g., perhaps there are some industries which we already can fully formalize, but which still work in the applied-science regime, because building the thing and testing it empirically is cheaper than hiring a mathematician and waiting ten years. But once math is solved, you’d be able to effectively go through dozens of prototypes per day for, say, $1000, while previously, each one would’ve taken six months and $50,000.
Are there such industries? What are they? I don’t know, but I think there’s a decent possibility that merely solving formal math would immediately make things go crazy.
One difficulty with predicting the impact of “solving math” on the world is the Jevons effect (or a kind of generalization of it). If posing a problem formally becomes equivalent to solving it, it would have effects beyond just speeding up existing fully formal endeavors. It might potentially create qualitatively new industries/approaches relying on cranking out such solutions by the dozens.
E. g., perhaps there are some industries which we already can fully formalize, but which still work in the applied-science regime, because building the thing and testing it empirically is cheaper than hiring a mathematician and waiting ten years. But once math is solved, you’d be able to effectively go through dozens of prototypes per day for, say, $1000, while previously, each one would’ve taken six months and $50,000.
Are there such industries? What are they? I don’t know, but I think there’s a decent possibility that merely solving formal math would immediately make things go crazy.