OpenAI shares a proposed Navier-Stokes proof as researchers debate credit

OpenAI has published a proposed solution to the Navier-Stokes existence and smoothness problem, releasing a mathematical paper and a formal proof written in Lean. The claim concerns one of the Clay Mathematics Institute’s Millennium Prize Problems: whether a smooth three-dimensional fluid flow can develop a breakdown in finite time.

The release arrives alongside a separate mathematical advance by Levent Alpöge and Tristan Buckmaster, and a public disagreement about the sequence of the research, credit and private data. Those questions sit beside a precise technical claim that readers can now inspect in the paper and code.

A smooth force and a shrinking vortex

OpenAI’s paper starts with a fluid at rest. For every positive viscosity, it constructs a smooth external force under which the fluid’s velocity becomes unbounded in finite time, while its kinetic energy remains bounded.

Viscosity describes the resistance that tends to smooth differences in motion. The construction concentrates increasingly fast motion into a shrinking region. Its difficult step is making the force stay smooth throughout this process. The paper uses oscillatory corrections to balance the terms that would otherwise become singular.

The official Clay formulation explicitly includes breakdown alternatives with a smooth force. OpenAI identifies its result with alternative C, for the whole three-dimensional space, and alternative D, for periodic space. The external force is therefore part of the stated problem that the authors address.

The written argument and the machine check

The Lean repository provides the formal statements, build instructions and an independent checking route using Comparator. It also contains an unforced Euler construction, where the viscosity term is absent.

Formal verification checks a proof against its encoded definitions and assumptions. Mathematical assessment also involves examining how those definitions express the intended problem. The public paper and repository give specialists both forms of the argument to examine. YFarmX’s review covers the theorem statement and supporting documents; full-proof validation requires specialist assessment.

Two research programmes and a disputed release

In his statement, Buckmaster describes a personal collaboration with Alpöge, using several language models. He credits Diego Córdoba and Luis Martínez-Zoroa with the programme that made their approach possible. Their released results cover smooth forcing for incompressible porous media, Boussinesq and three-dimensional incompressible Euler.

Buckmaster raises concerns about the timing of OpenAI’s effort and the handling of discussions over publication and authorship. He says he asked whether their private Codex sessions had entered model training, while explicitly acknowledging that he did not know whether their data had been used.

OpenAI’s response says its researchers and agents first saw the pair’s work when it became public, and that no specific user data was accessed to solve the problem. It leaves open the possibility that de-identified product-usage data contributed to model improvement. The company recognises the pair’s priority on forced Euler.

OpenAI dates the start of its effort to 1 September, following rumours of mathematical progress. It reports a successful group of roughly 10,000 concurrent agents, a Navier-Stokes result after about 88 hours and a further 17 hours for Lean formalisation and verification. These are the company’s account of its process.

The published material gives the debate a concrete centre: the exact theorem, the proof, the formal definitions and the chronology of the two research programmes.