qedbot

Breaking·First-hour kit

On the Navier–Stokes Millennium Prize Problem

D3 checkable OpenAI 8 Sep 2026

Both results carry a paper and a Lean formalisation checked with Comparator. Read the announcement.

The first hour

What is claimed, and how much can be inspected?

Navier–Stokes blowup with smooth forcing, and unforced Euler blowup. Of 2 results announced, 2 are named, 2 written up and 2 published with an artifact anyone can check.

Does the formal statement say what is claimed?

The formal statement is anchored: the proof is checked against a statement written independently of its authors.

  • Existence and Smoothness of the Navier–Stokes Equation: Formal statement held: FormalConjectures/Millennium/NavierStokes.lean. F3 anchored: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here. Flags: reviewed by its authors only, its anchor link points at a path the corpus has since renamed. Read the statement

Who did the work?

Graded A2 directed for who did the mathematics.

  • OpenAI internal model: A2 directed. By OpenAI's account some 10,000 agents worked for 88 hours with little human mathematical input. The run was aimed at a problem the Córdoba–Martínez-Zoroa programme had already brought within reach, and began after reports of the Buckmaster–Alpöge work reached OpenAI. A2 records a result the system produced on framing it was given.
  • GPT-6 Astra: A1 collaborative. Formalisation of a proof found by another system; the project's formalization.yaml records the method as an agent in Codex.

Who got there first?

Recorded: 2 precursors, 1 piece of concurrent work and 2 disputes.

  • Thomas Hou and Guo Luo: built on, 2013: Numerical evidence that solutions of the 3D Euler equations can blow up in finite time. Source
  • Diego Córdoba and Luis Martínez-Zoroa: built on, 2023: An analytic programme for constructing finite-time blowup, which with Fan Zheng gave unforced blowup for 3D Euler and forced blowup for hypodissipative Navier–Stokes. Both teams that reached the Millennium setting built on it. Source
  • Tristan Buckmaster and Levent Alpöge: concurrent, 2026-08-22, announced 2026-09-07: Blowup with smooth forcing for Euler, the incompressible porous media equation and Boussinesq, obtained on 15 August with AI assistance and verified in Lean a week later. Announced about twelve hours before OpenAI. Source
  • Priority and customer data: Buckmaster says news of the pair's progress reached OpenAI before its run, and asks whether their use of Codex informed the model. OpenAI's account changed between 8 and 13 September, ending with the statement that no user input after 3 July could have influenced the system. Source
  • Attribution: The first version of OpenAI's paper did not cite Córdoba and Martínez-Zoroa. The references were added in the 166-page revision. Source

What would move the grades

  • Evidence rises from V2 with an independent rebuild, by qed.bot or Palomar.

AI activity

How grades work
OpenAI internal model

8 Sep 2026

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.

full A2 V2 F3
Reasoning and sources

Autonomy

By OpenAI's account some 10,000 agents worked for 88 hours with little human mathematical input. The run was aimed at a problem the Córdoba–Martínez-Zoroa programme had already brought within reach, and began after reports of the Buckmaster–Alpöge work reached OpenAI. A2 records a result the system produced on framing it was given.

Details

compute: At least 10,000 agents over an 88-hour run from 1 September; 2.7 million messages and 130 billion output tokens in the run that produced the proof

paper: 166 pages, revised to cite Córdoba and Martínez-Zoroa

GPT-6 Astra

9 Sep 2026·supporting task

Formalised the Navier–Stokes and Euler results in Lean, checked with Comparator against the Formal Conjectures statements of alternatives (C) and (D).

full A1 V2 F3
Reasoning and sources

Autonomy

Formalisation of a proof found by another system; the project's formalization.yaml records the method as an agent in Codex.

Details

scale: 2,659 Lean files, about 33 MB of source

Provenance

Built on

  • Thomas Hou and Guo Luo 2013

    Numerical evidence that solutions of the 3D Euler equations can blow up in finite time. Source

  • Diego Córdoba and Luis Martínez-Zoroa 2023

    An analytic programme for constructing finite-time blowup, which with Fan Zheng gave unforced blowup for 3D Euler and forced blowup for hypodissipative Navier–Stokes. Both teams that reached the Millennium setting built on it. Source

Concurrent work

  • Tristan Buckmaster and Levent Alpöge 2026-08-22, announced 2026-09-07

    Blowup with smooth forcing for Euler, the incompressible porous media equation and Boussinesq, obtained on 15 August with AI assistance and verified in Lean a week later. Announced about twelve hours before OpenAI. Source

In dispute

  • Priority and customer data

    Buckmaster says news of the pair's progress reached OpenAI before its run, and asks whether their use of Codex informed the model. OpenAI's account changed between 8 and 13 September, ending with the statement that no user input after 3 July could have influenced the system. Source

  • Attribution

    The first version of OpenAI's paper did not cite Córdoba and Martínez-Zoroa. The references were added in the 166-page revision. Source

Prize

Clay Millennium Prize: OpenAI does not intend to claim it, and the Clay Mathematics Institute has acknowledged no party.

Sources

Citing this kit

qed.bot, “On the Navier–Stokes Millennium Prize Problem: first-hour kit”, https://qed.bot/a/openai-2026-09-08, as of 30 Sep 2026.

How the grades work