Universal computation in forced Navier–Stokes flows

Universal computation in forced Navier–Stokes flows concerns whether the incompressible Navier–Stokes equations, driven by a smooth external force, can carry out arbitrary computation: whether a finite program for the force can make a designated fluid particle reach a fixed region exactly when a given Turing machine halts. A family of manuscripts dated 27 September and 6 October 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims constructions of this kind on fixed flat three-dimensional domains, at any fixed positive computable viscosity and for a fluid starting at rest, so that the corresponding reachability problem is undecidable. The collection includes Lean formalizations of the main statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of A fixed particle test for computation in a forced viscous flow:
  • Turing showed that no machine decides whether an arbitrary described machine prints a designated symbol; the halting formulation follows by a finite modification. Moore's generalized shifts realize the local symbol changes and tape shifts of a machine as affine operations on real coordinates, the unbounded information being carried by exact real positions.
  • A smooth flow is invertible between two times, whereas a machine may overwrite symbols. Landauer's principle of retaining intermediate information and Bennett's reversible simulation, which records the executed instructions on a history tape, address this; the manuscripts use the same principle with a third real coordinate.
  • Cardona, Miranda, Peralta-Salas and Presas constructed stationary Euler flows on a three-sphere with an adapted Riemannian metric whose trajectories simulate Turing machines. Dyhr, González-Prieto, Miranda and Peralta-Salas obtained stationary unforced Navier–Stokes universality with an adapted metric and Hodge viscosity. Cardona, Miranda and Peralta-Salas also constructed universal steady Euler flows of infinite energy on Euclidean R³ and tape-bounded simulations on the flat three-torus.
  • In the manuscripts, the flat domain and the viscosity are fixed in advance and the fluid starts at rest; the machine and its input enter only through the force. The introduction states that the earlier results do not supply this construction.

The original results

• Claim. For a fixed positive computable viscosity and zero initial velocity, a terminating compiler turns a Turing machine and an input into a finite description of a smooth external force such that a fixed particle enters a fixed open set exactly when the machine halts. The manuscripts give several versions:
  • on the flat three-torus, with every mixed derivative of the force and the velocity bounded and square-integrable in time (A fixed particle test), with forces periodic from time zero (Geometric programs for solenoidal forcing), or with mean-zero forces that become stationary after time one (Eventually stationary forcing);
  • with velocity and force decaying faster than every inverse power of time and sharing one compact support for every machine and input (Rapidly vanishing forcing);
  • with halting detected by the velocity field itself: on the flat torus, the vertical velocity exceeds 1/2 somewhere in a fixed observation strip exactly when the machine halts, with an integral version on R² × T (Velocity-field detection);
  • on R³, one compactly supported velocity working for every viscosity ν > 0, with zero pressure and force f₀ + νf₁, built from incompressible transport of solid boxes (Incompressible box transport and finite computation).
• Method, as described: each construction prescribes an explicit smooth divergence-free velocity, sets the pressure to zero and defines the force as the residual of the equations; the solution is then unique in a stated energy comparison class. The velocity executes the machine's instructions on positional codes, records each selected branch in a further coordinate so that the flow stays invertible, and keeps the particle away from the detector during a nonhalting run; finer spatial gates are compensated by longer time steps. The fixed-particle manuscript states that it gives neither a uniform perturbation tolerance for arbitrarily long runs nor an efficient time bound.
• Sources (openai/math repository, commit 1581d4c):
  • A fixed particle test for computation in a forced viscous flow;
  • Universal computation with eventually stationary Navier–Stokes forcing;
  • Computation under rapidly vanishing Navier–Stokes forcing;
  • Velocity-field detection of computation in forced Navier–Stokes flows;
  • Geometric programs for solenoidal forcing;
  • Finite instructions and solenoidal shear flows;
  • Prefix instructions and incompressible flows;
  • Scalar potentials and slow clocks for forced fluid computation;
  • Incompressible box transport and finite computation (6 October; an earlier edition is dated 27 September).
• Formalization, as described by the repository. The scope note lists six Comparator statements: positive diagonal programs on incompressible coding sheets (SolenoidalSheetPrograms.lean), rapidly decaying alternating-coordinate memory (NavierStokesAlternating.lean), pointwise and integral velocity-field detection of halting (NavierStokesVelocity.lean), incompressible transport of solid boxes (BalancedBoxRouting.lean), finite computation in a balanced zero-data flow (BalancedThreeStack.lean) and effective finite computation detected by a fixed particle (ForcedNavierStokesComputation.lean).

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 20 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates this family "full" and records Comparator passes for all six challenges. Its note states that the force is derived from a prescribed flow as its residual, which it calls legitimate because the solutions are shown unique in an energy comparison class, and that the force must be uniformly computable from the machine and its input, which excludes a force that already knows the halting answer.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-08	RiScJ/ns-computer (GitHub; commit f51480b)	Use (implementation)	Builds explicit smooth solutions of the forced Navier–Stokes equations whose material flow performs shift-and-add multiplication and an eight-round Feistel cipher and its inverse, following the box-transport manuscript, and checks every hypothesis of the analytic lemmas it uses exactly for its instance. It also implements the manuscript's universal machine converter as a cross-check.	The README states that it was written by Claude Opus 5.5 under the author's guidance, that it treats one instance rather than the theorem, that the lemmas, the uniqueness argument and the Lean proofs are not re-verified, and that it says nothing about unforced fluids or the regularity problem.
2026-10-10	cert-machine, openai/math lane K: runs 38040214623 (BalancedBoxRouting) and 38051470892 (the other five challenges)	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept all six solutions, in 174 to 554 s each. The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists none of the six challenges of this family, so they were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee reviews of all nine manuscripts (328, 453, 475, 494, 496, 518, 529, 535, 544) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap in any of the nine manuscripts, with two minor notes: Scalar potentials and slow clocks does not say where its branch index starts. Starting at 0 would leave branch 0 unlifted; the reviewer states that the halting equivalence still holds and that indexing from 1 removes the ambiguity. In a specialization in Geometric programs for solenoidal forcing, two position bounds omit an offset of half a cell. The reviewer states that the corrected bounds leave the conclusion unaffected.	Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
2026-10-20 (latest commit)	jiamo/lambda-computability (GitHub, commit d35114f)	Use (Lean port)	A Lean library on lambda calculus and computability whose NOTICE file lists five files adapted from the collection's SolenoidalRecorder formalization for this family (Finite instructions and solenoidal shear flows), with the statement that "the mathematics and the proofs are upstream's".	GitHub repository (created before the release; the adaptation is listed in its NOTICE file).

Notes

• The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.