Setting aside the disagreement, I was very interested to see the net pricing of the discovery:
> All told, the week-long effort consumed 300 billion output tokens — $22.5 million worth of compute, if charged at current Astra rates.
> The Navier-Stokes existence and smoothness problem is one of the seven Millennium Prize problems — a set of major unsolved math problems, each carrying a $1 million bounty
I know openAI isn't solving these problems in order to make profit, but it's interesting to guess how close we are to these things becoming profitable. Eg, if you think their public pricing for Astra is ~2x as expensive as their internal price, then they lost ~10M on net for this proof. That's not profitable, but it is much better than I would have expected, which is exciting for the other Millennium prize problems! Of course the fundamental approach (which they may have plagiarized from Buckmaster and Alpoge) might have added cost to that as well. Nonetheless, I wouldn't be too surprised if they're all solved within the next 3 years!
I would assume they spent similar amounts on the other Millennium problems too. Also, they probably tried it before with older models.