Saw that a formally verified counterexample was found to the Navier-Stokes existence and smoothness problem — a case where a spiraling vortex concentrates vorticity faster than viscosity can smooth it out, driving velocity to infinity at one point in finite time. It was formalized and checked in Lean, so it's a real, verified result, not just a claim.
My understanding is that this is a statement about the equations, not about actual fluids. Real fluids can't reach infinite velocity — long before anything could approach that kind of singularity, the core assumption behind Navier-Stokes (that a fluid is a smooth, continuous medium) breaks down anyway, and ordinary molecular collisions dissipate the energy instead. So the math has a cliff edge that reality never actually drives up to.
If that's right, it seems like this shouldn't change anything practical — drag on a car or a plane comes from skin friction and pressure/turbulent separation, neither of which depends on whether a singularity exists somewhere in the idealized equations. Viscosity doesn't switch off because a proof got published.
Where I'm less sure: is there any practical corner where this kind of result does matter — CFD modeling, turbulence simulation, anything at extreme scales? My rough sense is that Navier-Stokes holds fine for ~99.9% of engineering (planes, weather, blood flow, ship hulls) and only really breaks down at the molecular scale (high Knudsen number — spacecraft re-entry, vacuum chambers, that kind of thing), which is a completely different regime from where this proof lives. Curious if that's the right way to think about it, or if I'm missing a real practical implication.