Description:

On September 8, 2026, OpenAI announced an AI-generated, Lean-verified proof that the 3D Navier–Stokes equations can blow up in finite time — but with a smooth external force applied. The Clay Millennium Prize problem is stated for the unforced equations (f = 0), and OpenAI has said it will not claim the prize. This market asks whether AI closes that gap this year.

Resolves YES if: before 11:59 PM ET December 31, 2026, a proof is publicly posted that resolves the Clay Institute's Navier–Stokes existence and smoothness problem as officially stated — i.e., for the unforced 3D incompressible equations with smooth, divergence-free, finite-energy initial data, in either the R³ or periodic setting — in either direction (finite-time blow-up, or global existence and smoothness), and the proof is credited by its authors as produced primarily by an AI system.

Terms:

• Must be the Clay statement. Blow-up with any external forcing, for averaged or modified Navier–Stokes, for Euler, or in dimensions other than three does NOT count. Blow-up from non-smooth or infinite-energy data does 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 that used AI as an assistant do not count; the Buckmaster–Alpöge working style — AI-found proof, Lean-verified, humans translating it — DOES count if they describe it that way.

• Announcement, not acceptance. Resolves YES on posting; later discovery of a formalization-statement mismatch or error does not reverse resolution. Clay recognition is not required.

• Any lab or team counts.

• Post-creation only. As of creation, no qualifying proof exists; OpenAI's September 8 forced result explicitly does not satisfy the unforced requirement.

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