qedbot

The Millennium Museum·Partial differential equations

Claimed by AI, not acknowledged

Navier–Stokes Existence and Smoothness

In three dimensions, do smooth, finite-energy solutions of the incompressible Navier–Stokes equations exist for all time, or can they break down in finite time?

Claimed. On 8 September 2026 OpenAI announced finite-time blowup with smooth forcing, Fefferman's alternatives (C) and (D), with a Lean formalisation. The Clay Institute has acknowledged no party, and OpenAI does not intend to claim the prize.

The exhibit

The problem, three ways

Curious

The Navier–Stokes equations describe how water and air move, and engineers use them every day. Yet nobody had proved that their solutions stay well behaved forever: could a smooth flow suddenly develop an infinitely sharp spike? In September 2026 OpenAI claimed that, pushed from outside in a carefully chosen smooth way, it can.

Undergraduate

The equations are ∂ₜu + (u·∇)u = νΔu − ∇p + f with ∇·u = 0, on ℝ³ or on the torus. The Clay description asks for one of four alternatives: smooth solutions for all time without forcing on ℝ³ (A) or the torus (B), or breakdown in finite time with smooth forcing on ℝ³ (C) or the torus (D). Leray proved in 1934 that weak solutions exist for all time; whether they stay smooth is the question.

Specialist

Partial regularity (Caffarelli, Kohn and Nirenberg) confines any singular set, and Tao's averaged equations showed that energy methods alone cannot rule out blowup. The Córdoba–Martínez-Zoroa programme constructs forced singularities; the 2026 claims push the forcing to C^∞ within Clay's decay and energy conditions, first for Euler, porous media and Boussinesq (Buckmaster and Alpöge), then for Navier–Stokes (OpenAI).

What would count

  • A proof of one of Fefferman's four alternatives exactly as stated, including the smoothness and decay conditions on the data and the forcing.
  • Clay's conditions: publication in a qualifying outlet, two years, general acceptance, then a decision by its board.

Fidelity traps

  • The Euler equations, hypodissipative equations and averaged equations are different problems.
  • The forcing must be smooth and meet Clay's decay bounds; a merely Hölder-continuous forcing does not count.
  • Alternatives (C) and (D) concern breakdown with forcing. They say nothing about the unforced alternatives (A) and (B).
  • OpenAI's formalisation is checked with Comparator against the Formal Conjectures statements of (C) and (D), which is why the register grades its fidelity F3.

In the register

Formal record: mixed

Formal statement: FormalConjectures/Millennium/NavierStokes.lean

  • OpenAI internal model 2026-09-08
    Finite-time blowup for the 3D incompressible Navier–Stokes equations with smooth forcing, on Euclidean space and on the torus: Fefferman's alternatives (C) and (D), a negative answer to the Millennium problem. Unforced Euler blowup is proved alongside.
    A2 directed · V2 artifact · F3 anchored
  • GPT-6 Astra 2026-09-09
    Formalised the Navier–Stokes and Euler results in Lean, checked with Comparator against the Formal Conjectures statements of alternatives (C) and (D).
    A1 collaborative · V2 artifact · F3 anchored

The full record →

Who is attacking it

  • OpenAI: Claims alternatives (C) and (D), from an 88-hour run of some 10,000 agents, with a Lean formalisation. Source
  • Tristan Buckmaster and Levent Alpöge: Blowup with smooth forcing for Euler, porous media and Boussinesq, found with AI assistance and verified in Lean. Source
  • Diego Córdoba, Luis Martínez-Zoroa and Fan Zheng: The analytic programme for constructing finite-time singularities that both teams built on. Source
  • A DeepMind collaboration of 22 authors: Numerical construction of unstable singularities for porous media and Boussinesq equations. Source

The history

15 events
  1. 19th century
  2. 1822

    posed

    Navier's equations

    Claude-Louis Navier derives equations of motion for a viscous fluid.

    Source

  3. 1845

    posed

    Stokes

    George Gabriel Stokes derives the equations independently, in the form still used.

    Source

  4. 1930s
  5. 1934

    progress

    Leray's weak solutions

    Jean Leray proves that weak solutions exist for all time. Whether they are smooth and unique is left open, and remains so.

    Source

  6. 1950s
  7. 1951

    progress

    Hopf

    Eberhard Hopf extends Leray's weak solutions to bounded domains; they are now called Leray–Hopf solutions.

    Source

  8. 1980s
  9. 1982

    progress

    Partial regularity

    Caffarelli, Kohn and Nirenberg show that any singular set of a suitable weak solution is small, of one-dimensional parabolic Hausdorff measure zero.

    Source

  10. 2000s
  11. 2000-05-24

    prize

    A Millennium Prize Problem

    The Clay Mathematics Institute names the problem one of seven carrying a $1,000,000 prize, with an official description by Charles Fefferman setting out four alternatives.

    Source

  12. 2010s
  13. 2013

    computation

    Numerical evidence of blowup

    Guo Luo and Thomas Hou present numerical evidence that solutions of the 3D Euler equations can blow up in finite time, shifting opinion about the answer.

    Source

  14. 2016

    barrier

    Averaged equations blow up

    Terence Tao constructs finite-time blowup for an averaged version of the equations, showing that arguments using only the energy identity cannot prove global regularity.

    Source

  15. 2019

    progress

    Singularities for Euler

    Tarek Elgindi proves finite-time singularity formation for C^(1,α) solutions of the incompressible Euler equations.

    Source

  16. 2023
  17. 2023

    progress

    The Córdoba–Martínez-Zoroa programme

    Diego Córdoba and Luis Martínez-Zoroa introduce new constructions of finite-time blowup; with Fan Zheng they reach unforced blowup for 3D Euler and forced blowup for hypodissipative Navier–Stokes.

    Source

  18. 2025
  19. 2025-09-17

    computation

    Unstable singularities

    A preprint by 22 authors from universities and DeepMind, including Buckmaster, demonstrates new numerical methods for constructing singularities of the porous media and Boussinesq equations.

    Source

  20. 2026
  21. 2026-08-15

    AI

    Smooth forcing for Euler

    Tristan Buckmaster and Levent Alpöge, working with AI models, obtain finite-time blowup with smooth forcing for Euler, porous media and Boussinesq. The results are verified in Lean a week later.

    Source

  22. 2026-09-07

    dispute

    Buckmaster's statement

    Shortly before midnight, Buckmaster announces the pair's results and says news of their progress reached OpenAI before its run began.

    Source

  23. 2026-09-08

    AI

    OpenAI claims alternatives (C) and (D)

    About twelve hours later, OpenAI announces finite-time blowup for Navier–Stokes with smooth forcing, from an 88-hour run of some 10,000 agents, with a 166-page paper and a Lean formalisation checked against the Formal Conjectures statement.

    Source · In the register

  24. 2026-09-11

    dispute

    A Severe Misalignment

    A declaration signed by 26 Fields Medalists warns against AI companies treating unsolved problems as benchmarks without adding to human understanding.

    Source

  25. Next
  26. ?

    The next entry

    Follow this problem below to get an email the moment it moves.

Follow and discuss

All discussion

Discussion and bounties for this problem load here.