Title: Will AI produce a proof of finite-time blow-up for the unforced Navier–Stokes equations before 2027?

Description:

On September 8, 2026, OpenAI announced an AI-generated, Lean-verified proof that the 3D incompressible Navier–Stokes equations can develop a finite-time singularity from smooth initial data under a smooth external force. That construction addresses options C and D of the Clay Institute's official problem statement, which permit a smooth forcing term satisfying specified decay conditions; Clay has said the problem is "apparently settled" pending its review.

This market is about a different and still-open question: the unforced equations (f ≡ 0). No external force is available to drive the singularity, and mathematicians have identified concrete obstacles to removing the force from the current construction. This market asks whether AI resolves the unforced case this year.

Resolves YES if: before 11:59 PM ET December 31, 2026, a proof is publicly posted that resolves, in either direction, the global regularity question for the three-dimensional incompressible Navier–Stokes equations with zero external forcing, for smooth, divergence-free, finite-energy initial data, in either the whole space R³ or the periodic setting — and the proof is credited by its authors as produced primarily by an AI system.

"Either direction" means: (i) a construction of smooth, finite-energy initial data whose solution loses smoothness in finite time, or (ii) a proof that all such initial data yield global smooth solutions.

Terms:

• Must be unforced. Any external forcing term, however smooth, compactly supported, or rapidly decaying, does NOT count. OpenAI's September 8 result and the Buckmaster–Alpöge results do not satisfy this market.

• Must be the 3D incompressible Navier–Stokes equations with positive viscosity. Euler, averaged or modified Navier–Stokes, hyperdissipative variants, other dimensions, or non-smooth / infinite-energy data do NOT count.

• Must be a claim of full resolution, not conditional or partial progress.

• Anti-crank filter: the proof must be either (i) formally verified in Lean, Coq, Isabelle, or an equivalent proof assistant with the formalization publicly available, or (ii) posted or endorsed by a frontier AI lab (OpenAI, Anthropic, Google DeepMind, xAI, Meta, or a comparable lab). Preprints meeting neither condition do not count regardless of author.

• AI as primary prover. The authors must describe the proof as generated by an AI system. Human proofs using AI as an assistant do not count; an AI-found, Lean-verified proof that humans then translate into readable form does count if the authors describe it that way.

• Announcement, not acceptance. Resolves YES on posting. Later discovery of an error or a formalization-statement mismatch does not reverse resolution. Clay Institute recognition is not required and is not the standard.

• Any lab or team counts.

• Post-creation only. As of creation, no qualifying proof exists.

• Resolution by the primary preprint or lab announcement, linked in comments.

Note (updated September 15): An earlier version of this description incorrectly stated that the Clay problem is defined only for the unforced equations. That was wrong — options C and D of the official statement admit smooth forcing — and the description has been corrected accordingly. The title and resolution target have not changed; this market has always been about the f ≡ 0 case.