AI Proved What?

Episode 376, October 2026

A fluid that computes?

Nine AI preprints claim universal computation in forced Navier–Stokes flows on a fixed flat domain

Covers result 376 in OpenAI’s catalog: all 9 papers. See its connections to other results and the work it cites.

Play Episode 376: A fluid that computes? A Turing tape above a sheared square and a detector strip.

4:26. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:14The claim
  3. 2:28How the proof goes
  4. 3:41Where it stands

The claim, in plain words

Can a fluid compute? In 1991 Cris Moore wrote that no one knows whether hydrodynamics, the Navier-Stokes equation for example, is capable of computation. Computing here means: any Turing machine and its input can be encoded into the setup so that some feature of the flow reveals whether the machine ever halts, a question that is undecidable in general. Our computer runs small machines: the two-state busy beaver halts after six steps, a four-state one after 107, while a machine that walks right forever never halts, and no finite run can certify that.

Ideal fluids came first: in 2021 Cardona, Miranda, Peralta-Salas and Presas built a steady, Turing-complete flow of an ideal fluid on a specially shaped three-sphere. For viscous flow, a July 2025 paper by Dyhr, González-Prieto, Miranda and Peralta-Salas built unforced, stationary, Turing-complete Navier-Stokes flows on specially deformed spaces, writing that the Navier-Stokes case had remained open until then. The open questions in that literature concerned flows without external forcing.

Result 376 is nine OpenAI papers, 260 pages, dated September 27 and made public October 6, 2026, with one revised the next day. The headline: on the flat three-dimensional torus, at any fixed positive computable viscosity, an algorithm turns any Turing machine and input into a smooth, divergence-free force. The flow that starts at rest under that force is unique, and a particle starting at a fixed point enters a fixed region exactly when the machine halts. So predicting that particle is undecidable.

What it doesn’t claim

The companion papers vary the setup: a force that becomes constant in time, one that is periodic from the very start, one that dies off faster than any power of time in ordinary space, or detection through the velocity itself. Not claimed: anything about unforced or natural flows, or robustness, since everything rests on exact positions. The force is tailored to each machine, and the papers say that making a chosen velocity a forced solution is elementary; the work is in the compiler and in tracking the particle at every moment.

Where it stands

Posted as a preprint
OpenAI, nine papers, 260 pages, dated September 27, 2026; one revised a day after release
Peer reviewed
Not yet; no specialist verdict
Formalized in Lean
Five theorems from four of the nine papers (scope notes); the headline theorem in an uncatalogued file (InitializedMain.lean)

Last checked October 19, 2026. The papers are unrefereed; one was revised a day after release, in supporting estimates rather than in its theorems. The catalogued Lean covers four of the nine papers, five theorems in about 52,000 lines; the headline theorem is proved in an uncatalogued Lean file of about 11,000 lines, and a larger uncatalogued hub covers more. We ran none of it. One comparator writes construction-specific definitions into its statement. We found no specialist verdict. OSVerify has not reviewed it.

How the proof goes

  1. A reversible machine, coded as a point. First the machine is made reversible with a seven-row recorder, in the style of Bennett. Our computer runs it on the two-state busy beaver: 84 microsteps, each one undoable, matching the paper’s step count. Then the tape is coded in base B as a point in a square, and each machine step becomes an exact affine move: a head move stretches one direction and squeezes the other. Our computer checks all six steps exactly, and shows how fragile the coding is: in our base-five version, tapes that differ only twenty cells from the head have codes about 4 × 10⁻¹⁵ apart.
  2. Shear flows that are exact solutions. Each rule gets its own height: lift, apply four shears that compose to the stretch, translate, and lower. Our computer checks exactly that four shears give the stretch, with no point straying from the rectangle’s center by more than twice its half-width. Shears carry no self-advection, nor do the lifts and slides, so the force defined as the time derivative minus viscosity times the Laplacian makes them exact Navier-Stokes solutions, and an energy argument gives uniqueness. Codes that never halt stay to the left, and the halting square sits inside the detector.

The numbers in the video

  • Ours: busy beavers halt after 6 steps (2 states), 21 (3 states) and 107 (4 states); the papers' reversible recorder runs the 2-state one in 84 microsteps, each undoable.
  • Ours: in a base-5 coding every machine step of the 2-state busy beaver is an exact affine map; tapes differing 20 cells from the head have codes about 4 × 10⁻¹⁵ apart.
  • Ours: four shears compose exactly to the stretch diag(2, 1/2), as in the headline paper's Lemma 3.1.
  • Lean: 286 files and 51,806 lines across the five catalogued closures; 73 files and 11,351 lines for the uncatalogued headline (counted by us; not run by us).

Read the source

The 9 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The question

Can a fluid compute? In 1991 Cris Moore wrote that no one knows whether hydrodynamics, the Navier-Stokes equation for example, is capable of computation. Computing here means: any Turing machine and its input can be encoded into the setup so that some feature of the flow reveals whether the machine ever halts, a question that is undecidable in general. Our computer runs small machines: the two-state busy beaver halts after six steps, a four-state one after 107, while a machine that walks right forever never halts, and no finite run can certify that. Ideal fluids came first: in 2021 Cardona, Miranda, Peralta-Salas and Presas built a steady, Turing-complete flow of an ideal fluid on a specially shaped three-sphere. For viscous flow, a July 2025 paper by Dyhr, González-Prieto, Miranda and Peralta-Salas built unforced, stationary, Turing-complete Navier-Stokes flows on specially deformed spaces, writing that the Navier-Stokes case had remained open until then. The open questions in that literature concerned flows without external forcing.

1:14The claim

Result 376 is nine OpenAI papers, 260 pages, dated September 27 and made public October 6, 2026, with one revised the next day. The headline: on the flat three-dimensional torus, at any fixed positive computable viscosity, an algorithm turns any Turing machine and input into a smooth, divergence-free force. The flow that starts at rest under that force is unique, and a particle starting at a fixed point enters a fixed region exactly when the machine halts. So predicting that particle is undecidable. The companion papers vary the setup: a force that becomes constant in time, one that is periodic from the very start, one that dies off faster than any power of time in ordinary space, or detection through the velocity itself. Not claimed: anything about unforced or natural flows, or robustness, since everything rests on exact positions. The force is tailored to each machine, and the papers say that making a chosen velocity a forced solution is elementary; the work is in the compiler and in tracking the particle at every moment.

2:28How the proof goes

First the machine is made reversible with a seven-row recorder, in the style of Bennett. Our computer runs it on the two-state busy beaver: 84 microsteps, each one undoable, matching the paper’s step count. Then the tape is coded in base B as a point in a square, and each machine step becomes an exact affine move: a head move stretches one direction and squeezes the other. Our computer checks all six steps exactly, and shows how fragile the coding is: in our base-five version, tapes that differ only twenty cells from the head have codes about 4 × 10⁻¹⁵ apart. Each rule gets its own height: lift, apply four shears that compose to the stretch, translate, and lower. Our computer checks exactly that four shears give the stretch, with no point straying from the rectangle’s center by more than twice its half-width. Shears carry no self-advection, nor do the lifts and slides, so the force defined as the time derivative minus viscosity times the Laplacian makes them exact Navier-Stokes solutions, and an energy argument gives uniqueness. Codes that never halt stay to the left, and the halting square sits inside the detector.

3:41Where it stands

The papers are unrefereed; one was revised a day after release, in supporting estimates rather than in its theorems. The catalogued Lean covers four of the nine papers, five theorems in about 52,000 lines; the headline theorem is proved in an uncatalogued Lean file of about 11,000 lines, and a larger uncatalogued hub covers more. We ran none of it. One comparator writes construction-specific definitions into its statement. We found no specialist verdict. If they hold, a viscous fluid driven by a suitably programmed force can carry out any computation, so some questions about such forced flows are undecidable.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.