Terence Tao (npub1gve…sduy) writes: "For the first time in the history of mathematics, we are faced with the situation that open problems in pure mathematics -- one of the primary fuels for mathematical discovery -- are being mined as a non-renewable resource".
Very important thought!
But maybe it's renewable if one is willing to solve an already solved problem without looking at the existing solution. I sometimes fantasize about a far future world where everything I could prove has already been proved. That wouldn't need to stop me from making new discoveries, since the interesting part in math not just *whether* P implies Q, but *how*.
If everything interesting had already been proved in all interesting possible ways, there still might be room for me to create my own attractive outlook on mathematics, mainly by leaving things out.
“The sculpture is already complete within the marble block, before I start my work. It is already there, I just have to chisel away the superfluous material.”
― Michelangelo
However, as observed in Section 14.1, there were noticeable opportunity costs with moving too rapidly. We noted a few cases where a key implication stumped us for a while, and forced us to come up with interesting new techniques to construct infinite counterexamples to that implication; but subsequently it was found via an automated theorem prover that the implication in question actually had a relatively small finite counterexample. But if that counterexample had been found first, we might not have discovered the more interesting method. We in fact suspect that some of our early automated sweeps to resolve implications may have accidentally obscured some potentially fruitful problems that would have revealed even more constructions or insights, although we do not have the counterfactual data to confirm these suspicions definitively. For better or for worse, the ETP problem set is now "solved", and there is no practical way to undo this and recreate the unsolved status of this problem to encourage further exploration.
For the first time in the history of mathematics, we are faced with the situation that open problems in pure mathematics -- one of the primary fuels for mathematical discovery -- are being mined as a non-renewable resource; and if the solution is extracted poorly from that resource, then the net value to mathematics gained as a result can be significantly less than if it were obtained in a responsible and sustainable fashion. (2/3)