OpenAI
The group produced an analytical proof and Lean formalization that via Navier-Stokes dynamics a fluid can develop a singularity in finite time. The solution is a vortex, a spinning swirl of fluid, that spirals inward and gets increasingly elongated, like spaghetti.