But attempts to resolve either of these two questions have historically led to fundamental insights and influential theorems in fluid mechanics, analysis, and partial differential equations: the Leray-Hopf weak solutions, the Gagliardo-Nirenberg-Ladyshenskaya inequalities, the Prodi-Serrin partial regularity theorems, the Beale-Kato-Majda blowup criterion, the Escuriaza-Seregin-Sverak conditional regularity result, and so forth. The broader theory of turbulence, while not directly connected to any of these results, has certainly been informed at a philosophical level at least by the efforts to establish or disprove global regularity. One of my own contributions to the subject was to introduce the concept of fluid computation and Turing universality to the problem, which among other things led to the unexpected connections with symplectic topology. (2/6)
But attempts to resolve either of these two questions have historically led to fundamental insights and influential theorems in fluid mechanics, analysis, and partial differential equations: the Leray-Hopf weak solutions, the Gagliardo-Nirenberg-Ladyshenskaya inequalities, the Prodi-Serrin partial regularity theorems, the Beale-Kato-Majda blowup criterion, the Escuriaza-Seregin-Sverak conditional regularity result, and so forth. The broader theory of turbulence, while not directly connected to any of these results, has certainly been informed at a philosophical level at least by the efforts to establish or disprove global regularity. One of my own contributions to the subject was to introduce the concept of fluid computation and Turing universality to the problem, which among other things led to the unexpected connections with symplectic topology. (2/6)
With recent advances in understanding related fluid equations, it is now the emerging consensus that the answer to the global regularity problem for Navier-Stokes is negative: there should exist very specific initial conditions to this problem that develop singularities in finite time. There is even a reasonably well-defined strategy to locate such conditions:
(a) Design a nearly-self-similar ansatz for a finite time blowup solution.
(b) Locate an approximate solution to this ansatz, which numerically obeys the ansatz up to an extremely small, computable residual.
(c) Demonstrate that, in suitably renormalized coordinates, the ansatz is stable around this numerical solution, and can be perturbed into an exact solution if the residual is small enough.
(d) Verify that the residual of the solution falls within the threshold of stability of the solution.
(3/6)
The problem is that all of these steps are incredibly complicated, and interlock with each other. Many naive ansätze for these solutions can be ruled out to exist for various reasons, such as violation of conservation of energy. Other ansätze might initially seem viable, but could only be ruled out after extremely intensive numerical computation.
Nevertheless, it seems potentially possible that a heroic combination of machine learning-powered simulation, rigorous interval arithmetic and/or formalization, and LLM-generated proposals for a suitable ansatz, all guided by expert human mathematicians iteratively learning from previous attempts, could resolve this problem. The final construction would likely be enormously complicated, and impossible to verify by purely human means; the verification of it in a formal language such as Lean may end up being among the largest such proof artefacts ever created. (4/6)
But such an incomprehensible proof would not be the primary value of the exercise. The process of starting with one ansatz, discovering the precise obstruction preventing it from working, adjusting the ansatz to (partially) eliminate that obstruction, and then iterating, would almost certainly reveal important new insights about fluid mechanics that would not have been feasible to obtain by other means. Crucially, this iteration would only work well at producing such insights if the iterator did not have access to the final ansatz in advance, as this naturally inhibits the exploration of alternate routes to the ansatz that are superficially "dead ends", but in fact end up being highly instructive in the nature of their failure.
But there is now a scenario in which an autonomous AI harness, backed by an enormous amount of computational resources, performs this entire iteration internally, and ends up producing the final ansatz, and thence the solution to the Navier-Stokes regularity problem, while the AI company running the harness keeps the process to arrive at that ansatz almost completely out of public view. Technically, one of the most prominent open problems in mathematics would now be solved; but there would be almost no value added to mathematics as a consequence. It is theoretically possible that with some herculean (and heavily AI-assisted) additional effort by a third party, some portion of the process could be reverse-engineered to recover some actual insight and understanding from the solution; but this would be a far less efficient process than if the solution had been obtained via a diverse combination of both human mathematicians and machine assistance as mentioned above. (5/6)
