I think it's extremely damning that even Tao, who is very involved with OpenAI, recognises this for what it is: a false promise, a contribution to mathematics which leads to dead-ends in our theories and understanding, a company using unsolved conjectures as a resource to fuel their stock prices while providing little to no value back to the field of mathematics.
I hope that in the next couple years we as mathematicians seriously reconsider our current system where theorems proven/disproven are the primary social currency of mathematics, because these LLMs are hijacking these incentives in ways that are very damaging to us.
As an early-career researcher it's hard to not want to jump ship right now. I started doing mathematics very young and I have never loved something like I love maths, but all of the recent news makes me wonder whether it's actually a good idea to continue doing math.
Almost every single PhD student I have talked to is doubting whether they have a future with the current situation, and I hope we can figure things out before the current generation of mathematicians PhDs arrive into a world of maths that has been mined out and left barren by AI companies pumping more speculative value into their bubble.
(1/3)
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)