Meaningless Clay Navier-Stokes Problem Solved by AI

OpenAI announces a proof of existence of a solution to the Navier-Stokes equations (but not its numerical values), which starting from zero under smooth forcing ceases to exist in finite time: 

• We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean.

Charles Fefferman, who formulated the problem in precise mathematical terms, is along with other leading mathematicians such as Terence Tao, happy that the understanding of fluid motion has now taken a big leap forward by mathematical analysis, even if the development of the singularity cannot be followed in any precise terms. Something goes wrong but what and how is hidden.

There is a further problem in this happy moment, which I have complained about over the years: Fefferman's formulation misses the essence of the physics of fluid motion, namely turbulence. The Clay problem is sold as concerned with basic aspects of fluid motion,  but does not address the most fundamental problem of all of turbulence. Fefferman's formulation directs the interest away from physics, and the unhappy result is that solution now presented by AI covering 167 pages cannot be read to learn anything, simply a mess of formulas and theorems. 

This is certainly a memento for mathematics: AI can now produce proofs of an endless number of mathematical problems without real meaning, proofs which cannot be understood by mathematicians in detail only verified formally by Lean. What will be the result?

Numerical mathematics offers a solution to the fundamental problem of turbulence, thus a different solution to a different problem formulation. See tags to this post starting with this post from 2013.

Recall that slightly viscous flow is unstable from shear and stretch and so develops into non-smooth turbulent flow which however does not break down like the Clay solution. So the solution of physical interest is non-smooth and non-singular, which is not captured in Fefferman's dichotomy of smooth or singular.  

Turbulence is an extreme form of the design of a complex world with a variety of phenomena on different scales: Develop growth from instability + curb growth to allow continued existence, not captured by Fefferman's formulation.  

PS1 When I 20 years ago complained to Fefferman that his formulation lacked true interest from physics point of view, he returned that it was enough that the problem was interesting to him.

PS2 Note that the AI solution is a proof of the existence of a very special function (unknown to details) which is a solution with a very specific particular forcing. This is not the real setting which is to study solutions under general forcing. 

PS3 Here is an interesting catch of the AI proof of existence of a singular solution. Computational solutions can be constructed for general data including turbulence and any such solution can be viewed as an AI proof of existence performed by a computer according to strict mathematical principles, including evaluation of quality. The whole process can be seen as an AI proof of existence of a solution for each given set of data. It would be strange to not consider that as a solution to the essence of the Clay problem albeit not captured in Fefferman's formulation. 

PS4 Allowing AI as computational process into the Clay problem game, we may compare the Open AI proposal as an analytical AI proof of non-existence in a very special case, with an computational AI proof of existence for any data, except one. Which proposal would you give the money to? Or 50-50? Note that the estimated cost of the OpenAI solution is several million dollars, so the Prize money will not suffice to cover, what remains is fame at price of a couple million dollars, fine for OpenAI but not for a poor pure mathematician. 

PS5 The verification by Lean in principle requires each step to be verified from logic and previous axioms/therorems/steps, which is overwhelming and cannot be done. Compare with a numerical solution produced in a number of computational steps, where a verification of solution quality can be made without verifying each step (involving round-off which propagates) because the solution produced is known. Not so with the singular solution proved to exist by AI and so only stepwise check is available (which is more impossible than possible). 

PS6 The size of the forcing appears to scale with the square root of the viscosity which means that the constructed solution is not turbulent. Another sign that the problem formulation misses the essence of Navier-Stokes. How could it go so wrong for so many mathematicians?