I never understood why the Millennium Prize Navier-Stokes formulation asked for proof with f(x,t)=0 while counterexamples could have arbitrary smooth f(x,t). A counterexample with smooth f latter doesn't automatically serve as a counterexample to the first formulation.
It's always bugged me that it seems like we could end up in a situation where blow-up is proven for smooth f(x,t) but existence and smoothness is proven for f(x,t)=0.
The f asymmetry goes the other way too of course. Proving existence and smoothness with f=0 does not rule out breakdown for specific combinations of smooth u0 and f.
The reason I'm writing about this now is, of course, the OpenAI shitshow. I'm not going to go into the discussion around scooping and academic credit other than to say that if the account of Tristan Buckmaster is even remotely true, then it's really bad.
So, if the OpenAI result is verified, we have at least one set of initial conditions u0 and f(x,t) that leads to finite-time blow-up. This solves the Millenium Prize formulation, but leaves open the behaviour of the equations when f(x,t)=0.
From my understanding, they created a very specific forcing meaning that the result is less "general" in a sense that the Scientific American writeup almost calls cheating. So I guess, I'm not the only one annoyed by the counterexample formulation.