Post by @tao@mathstodon.xyz

2026-09-03 15:38 UTC

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)

Replies (1)

@tao@mathstodon.xyz 2026-09-03 15:38

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)

Open ##5125049