AI pushes Navier-Stokes toward a $1M prize

Anthropic and OpenAI models helped two mathematicians produce three results on equations adjacent to Navier–Stokes, the Millennium problem carrying a $1 million prize. The reported mathematical advance says two results have Lean formalizations and a third awaits formalization; the work concerns Boussinesq and Euler cousins, not full Navier–Stokes, so this is progress toward the problem rather than a solution. For builders, Claude’s Fermat proof is the useful precedent: let models search, but make machine-checkable formalization the release gate.