Interesting developments tonight, as Levent Alpöge and Tristan Buckmaster announce that after a fair amount of work they have constructed examples of finite-time blowup for a broad class of PDEs including 3-d incompressible Euler, inspired by of Diego Córdoba and Luis Martínez-Zoroa, and using plenty of LLM iteration in order to get the details right. This is, of course, a problem in the neighborhood of Navier-Stokes (in the negative direction of finding a counterexample to the conjecture, which I have over the years heard many PDE folks saying was the right way to bet), and Terry Tao says in a Mastodon thread that in principle this method doesn’t seem so far from showing blowup for Navier-Stokes too, though a large amount of compute and detail-checking would be involved.
At least part of this has already been Lean-formalized, though perhaps eccentrically I find I care a little less about that. What matters is not whether there’s an example but whether the example has something to teach us. An interesting but incorrect example would surely be of more value than an uninteresting but correct one. Well, I suppose the latter would have more financial value. Though even on that Millennium Prize page, one sees: “Why ask for a proof? Because a proof gives not only certitude, but also understanding.” Very true! We mustn’t settle for mere certitude. Certainly the work of Alpöge, Buckmaster, Córdoba, and Martínez-Zoroa seems to offer understanding as well.