Terence Tao on Nostr: However, as observed in Section 14.1, there were noticeable opportunity costs with ...

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)