Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Universal computation in forced Navier–Stokes flows

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Constructs viscous incompressible flows starting from rest on a fixed flat three-dimensional domain that perform universal computation under smooth external forcing. A terminating compiler turns a Turing machine and input into a finite program for the force, so a designated particle reaches a fixed region exactly when the machine halts. The viscosity is fixed, positive and computable. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

Both independent assessments find that the Lean statements express or imply the whole result described above. Read the assessments

Nine current papers; one replaced by a later edition.

The paper states

Theorem 1.1 (Eventually steady forcing)

In Universal Computation with Eventually Stationary Navier–Stokes Forcing, 27 September 2026

Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.

13 other possible matches are listed below the card, among them Theorem 4.1 (Rapid decay with alternating memories) in Computation under Rapidly Vanishing Navier–Stokes Forcing and Theorem 5.1 (Periodic lattice memory) in Computation under Rapidly Vanishing Navier–Stokes Forcing.

Fix a positive computable viscosity \nu. There is an effective procedure taking a deterministic Turing machine and finite input to a body force f on the flat torus \mathbb T^3, such that:

  1. 1.

    f is smooth on \mathbb T^3\times[0,\infty), has zero spatial mean, and is independent of time for t\ge1. Every spatial, temporal, and mixed derivative of f is bounded on this entire domain.

  2. 2.

    With initial velocity zero, the Navier–Stokes equation has a global smooth solution, unique in the classical class on every finite time interval. Its kinetic energy is bounded uniformly in time.

  3. 3.

    For the fixed particle label and fixed open set

    P=(1/4,1/4,0),\qquad \mathcal O=\{(X,Y,Z)\in\mathbb T^3:1/32<Y<1/8\},

    the material trajectory from P enters \mathcal O at a finite time if and only if the machine halts on the input.

The force is specified by a finite formula which does not simulate the chosen execution. The construction is also uniform as a formula in an arbitrary positive parameter \nu.

No Lean statement in the release is paired with this theorem.

13 more possible matches

  • Theorem 4.1 (Rapid decay with alternating memories) in Computation under Rapidly Vanishing Navier–Stokes Forcing, 27 September 2026.
  • Theorem 5.1 (Periodic lattice memory) in Computation under Rapidly Vanishing Navier–Stokes Forcing, 27 September 2026.
  • Theorem 1.1 in Scalar Potentials and Slow Clocks for Forced Fluid Computation, 27 September 2026.
  • Theorem 3.1 (Compact support and rapid decay) in Computation under Rapidly Vanishing Navier–Stokes Forcing, 27 September 2026.
  • Theorem 1.1 (Initialized computation by a solenoidal force) in Finite Instructions and Solenoidal Shear Flows, 27 September 2026.
  • Theorem 1.1 (Interspersed history on moving sheets) in Prefix Instructions and Incompressible Flows, 27 September 2026.
  • Theorem 1.1 (Periodic initialization) in Geometric Programs for Solenoidal Forcing, 27 September 2026.
  • Theorem 1.1 in Velocity-Field Detection of Computation in Forced Navier–Stokes Flows, 27 September 2026.
  • Theorem 8.4 (A separate one-unit loader on the torus) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Theorem 4.1 (Balanced three-stack realization) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Theorem 1 in A Fixed Particle Test for Computation in a Forced Viscous Flow, 27 September 2026.
  • Theorem 1.2 (General diagonal maps on a sheet) in Geometric Programs for Solenoidal Forcing, 27 September 2026.
  • Theorem 3.4 (Expansion, obstacle detours, and delivery) in Incompressible Box Transport and Finite Computation, 6 October 2026.
Reported proof verification
Six Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
Papers and explanations
Nine current papers, each readable here as a page beside its PDF. One explanation by others.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Finite Instructions and Solenoidal Shear Flows

27 September 2026, current edition.

Read it herePDF

We realize finite reciprocal affine instruction maps by smooth incompressible shear flows on a flat three-torus. Applied to a reversible one-head recorder with a finite transition table, this gives a complete machine-to-fluid construction: a fixed particle enters a fixed open strip exactly when a given machine halts, with zero initial velocity, zero pressure, and a solenoidal mean-zero force that is periodic after initialization. The construction acts on full closed rectangles and controls every intermediate trajectory. Separate heights resolve overlap between sources and targets, and an endpoint-size estimate controls all excursions independently of the reciprocal scaling factor.

A Fixed Particle Test for Computation in a Forced Viscous Flow

27 September 2026, current edition.

Read it herePDF

We construct smooth external forces for incompressible Navier–Stokes flow on a fixed flat three-torus at any fixed positive computable viscosity, from zero initial velocity, such that a fixed particle enters a fixed open set exactly when a prescribed Turing machine halts. Every mixed derivative of the force and velocity is bounded and square-integrable in time in spatial supremum norm. The construction uses the machine’s ordinary instructions, records their history in a third coordinate, and compensates for finer spatial gates by longer time steps.

Universal Computation with Eventually Stationary Navier–Stokes Forcing

27 September 2026, current edition.

Read it herePDF

At every fixed positive computable viscosity, we construct smooth mean-zero forces on the flat three-torus that become stationary after time one and make a fixed particle, initially in a fluid at rest, enter a fixed open set exactly when a prescribed Turing machine halts. The force has bounded derivatives of every order and a finite effective description. A reversible recording table is realized on whole planar rectangles by Hamiltonian motions, then driven by a mean-zero spatial clock. Separate choices give periodic forcing from time zero or a force whose derivatives are square-integrable in time.

Geometric Programs for Solenoidal Forcing

27 September 2026, current edition.

Read it herePDF

We construct smooth solenoidal mean-zero forces, periodic from time zero, for which a fixed particle on a flat three-torus reaches a fixed open strip exactly when a given machine halts. The initial fluid velocity and the pressure are zero. We also realize positive diagonal maps on coding sheets by incompressible shears, with explicit normal compensation for changes of planar area, and reciprocal maps on whole boxes of positive thickness. Complete local inverses, initialization rules, and intermediate trajectory bounds connect these geometric constructions to finite computations.

Prefix Instructions and Incompressible Flows

27 September 2026, current edition.

Read it herePDF

Finite prefix instructions may change area and erase information. We give explicit history processors and smooth incompressible motions that retain that information and realize every instruction on its full domain. A first application assigns each machine and finite input a smooth mean-zero force on the flat unit three-torus, at any fixed positive computable viscosity. The solution starts from rest; a fixed particle enters a fixed open strip exactly when the machine halts. The force repeats with period one after an initial loading interval. We then prove alternative realizations using full boxes, normal compensation, invariant planes, and a spatial clock. The constructions specify their initialization, comparison class, derivative bounds, and continuous-time observation. Exact formulas and effective cutoffs provide finite descriptions of the fields and all their derivatives.

Computation under Rapidly Vanishing Navier–Stokes Forcing

27 September 2026, current edition.

Read it herePDF

At any fixed positive computable viscosity, smooth forces can make a fixed fluid particle detect the halting of an arbitrary machine, starting from rest, while every mixed derivative of the force and velocity decreases faster than every inverse power of time. We give three complete memory constructions: compact moving curls, alternating fractional coordinates, and a periodic lattice on the flat three-torus. Each machine step takes one unit of physical time. The constructions retain earlier records at separated spatial scales and use an exact open detector with a shrinking signal.

Velocity-Field Detection of Computation in Forced Navier–Stokes Flows

27 September 2026, current edition.

Read it herePDF

We construct smooth forces for three-dimensional incompressible Navier–Stokes flow, from rest at any fixed positive computable viscosity, whose velocity field detects whether a prescribed machine halts. On the unit flat torus, a pointwise test of the third velocity component uses successively shorter stirring intervals in a fixed spatial region. On \(\mathbb R^2\times\mathbb T\), an integral test uses an expanding array of translation regions and a force with globally bounded mixed derivatives. The vertical velocity solves an advection–diffusion equation: short bursts control its pointwise error in the first construction, and a moving cutoff controls the total escaped mass in the second.

Scalar Potentials and Slow Clocks for Forced Fluid Computation

27 September 2026, current edition.

Read it herePDF

We construct smooth forces of fixed compact spatial support for three-dimensional incompressible Navier–Stokes flow from rest whose particle at the origin detects halting by entering a fixed half-space. Every mixed derivative of the force and velocity decays at rate \(O((1+t)^{-1-j})\) for time order j. Three scalar potentials lift a coded rectangle, perform its instruction, and lower its image; an unbounded logarithmic clock supplies the decay. We also realize area-changing prefix instructions on an invariant torus plane, and construct a planar Hamiltonian processor admitting periodic forcing, stationary forcing after startup, and a velocity-field detector through a companion diffusion theorem.

Incompressible Box Transport and Finite Computation

6 October 2026, current edition.

Read it herePDF

This version supplies effective torus-projection and common-clock decay estimates, including the projected-force and pressure bounds; see the previous version.

Earlier editions: 27 September 2026

We realize finite positive diagonal affine maps of determinant one by effective smooth incompressible flows on neighborhoods of entire closed rational solid boxes. The source and target families are each disjoint, but may overlap each other. The construction uses localized curls, evacuation to storage and obstacle detours. A balanced three-stack recorder then assigns every machine and finite input a smooth Navier–Stokes force with one compact spatial support, periodic after a loading interval, at any fixed positive computable viscosity. The fluid starts at rest, and one fixed particle enters one fixed open cube exactly when the machine halts. Further constructions give fixed torus charts, periodicity from time zero, alternative history guards and bounded or slab observers. Onto slow clocks yield separate decaying forces. Each construction includes an all-time observation proof, effective derivative bounds and a stated pressure comparison class.

Previous editions

Six Lean statements in this family

Choose one to see it beside the paper theorem it is paired with.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

ForcedNavierStokesComputation

The paper states

Theorem 5.1 (Periodic lattice memory)

In Computation under Rapidly Vanishing Navier–Stokes Forcing, 27 September 2026

Fix a computable viscosity \nu>0. A finite deterministic machine and a finite input effectively determine a smooth force g on the unit flat torus \T^3=(\R/\mathbb Z)^3 with zero spatial mean. The Navier–Stokes equations with force g and zero initial velocity have a smooth solution (U,0) with zero spatial mean. Its particle from

a_*=(1/4,1/2,1/2)

enters the fixed open set

O=\{x\in\T^3:1/2<x_1<1\pmod 1\}

at some finite time if and only if the machine halts on that input. For every pair of nonnegative integers r,J and every spatial multi-index \alpha, there is an effective constant C_{r,\alpha,J} such that

\|\partial_t^r\partial_x^\alpha U(t)\|_\infty +\|\partial_t^r\partial_x^\alpha g(t)\|_\infty \le C_{r,\alpha,J}(1+t)^{-J},\qquad t\ge0.

There is also an effective smooth mean-zero solenoidal force f with the same bounds and exactly the same velocity and material event. It is f=g-\nabla\phi, with pressure -\phi, where \phi is the mean-zero periodic solution of \Delta\phi=\operatorname{div}g.

For either force, uniqueness holds among periodic classical solutions for which the velocity, its time derivative and its spatial derivatives through order two, and the pressure and its spatial gradient, are continuous on every [0,T]\times\T^3. Pressure is normalized to have zero spatial mean.

The words they share: among, bounds, computable, derivative, derivatives, effective, enters, exactly, finite, fixed, flat, force, halts, holds, input, machine, material, mean, memory, navier, nonnegative, open, particle, periodic, pressure, smooth, solution, solutions, spatial, stokes, time, torus, uniqueness, unit, velocity, viscosity, zero.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Effective finite computation detected by a fixed particle

ForcedNavierStokesComputation.lean, the release lists it as a supporting statement.

theorem balanced_three_stack_realization :    ∃ U f₀ f₁ : Family Velocity,    ∃ X : Family MaterialFlow,    ∃ repeated : FiniteMachine → Velocity,      EffectiveFamily U ∧ EffectiveFamily f₀ ∧ EffectiveFamily f₁ ∧      (∀ M, Function.Periodic (repeated M) 1) ∧      ∀ (M : FiniteMachine) (w : Input M),        Smooth (U M w) ∧ Smooth (f₀ M w) ∧ Smooth (f₁ M w) ∧        f₀ M w = inertialCoefficient (U M w) ∧        f₁ M w = viscousCoefficient (U M w) ∧        CommonCompactSupport (U M w) (f₀ M w) (f₁ M w) ∧        BoundedMixed (U M w) ∧        PeriodicAfterOne (U M w) ∧        (∀ t, 1 ≤ t → ∀ x, U M w t x = repeated M t x) ∧        ComparisonClass (U M w) (fun _ _ => 0) ∧        IsMaterialFlow (U M w) (X M w) ∧

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

BalancedBoxRouting

The paper states

No paper theorem is paired with this Lean statement.

no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.

Statements it shares words with:

  • Proposition 13.5 (Full solid boxes with a height guard) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Proposition 13.1 (Ordered full-box transport) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Theorem 3.4 (Expansion, obstacle detours, and delivery) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Proposition 13.7 (Column and layer transport) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Proposition 13.3 (Simultaneous full-box transport) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Theorem 12.2 (Two bounded-box material tests) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Theorem 4.1 (Balanced three-stack realization) in Incompressible Box Transport and Finite Computation, 6 October 2026.
  • Theorem 4.1 (A smooth planar processor) in Universal Computation with Eventually Stationary Navier–Stokes Forcing, 27 September 2026.

The Lean statement

No paper theorem is paired with it.

Incompressible transport of solid boxes

BalancedBoxRouting.lean, the release lists it as a supporting statement.

theorem balanced_box_routing    (n : ℕ) (a b h k : Fin n → RationalSpace)    (hh : ∀ i j, 0 < h i j) (hk : ∀ i j, 0 < k i j)    (ha : Pairwise fun i j => Disjoint (solidBox (a i) (h i)) (solidBox (a j) (h j)))    (hb : Pairwise fun i j => Disjoint (solidBox (b i) (k i)) (solidBox (b j) (k j)))    (hvol : ∀ i, ∏ j : Fin 3, k i j / h i j = 1) :    ∃ U : Field, ∃ Φ : ℝ → Space → Space,      AdmissibleField U ∧ IsGlobalFlow U Φ ∧ Delivers a b h k Φ := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

BalancedThreeStack

The paper states

Theorem 1.1

In Velocity-Field Detection of Computation in Forced Navier–Stokes Flows, 27 September 2026

For each positive computable \nu, a machine and a finite input effectively determine each of the following two forces.

  1. 1.

    On \T^3, a smooth force has a unique global smooth solution in the torus class above, with pressure zero, for which (2) holds exactly when the machine halts. The force is supported in K\times\T for a compact K\subset(0,1)^2 independent of time. Its derivatives are bounded on every finite time interval; their bounds may grow with that interval.

  2. 2.

    On \R^2\times\T, a smooth force and all its mixed derivatives are globally bounded. On each finite time interval its horizontal support is compact. It has a unique global smooth solution in (4), with pressure zero and integrable nonnegative third component. Event (3) holds exactly when the machine halts.

The sets and thresholds in both observations are independent of the machine and input. The compact set K in the first construction may depend on that instance, but is independent of time. Both force prescriptions install all the required local instructions, without executing the selected computation.

The words they share: eq, comparison, compact, supported, input, computable, machine, pressure, finite, mixed, time, smooth, halts, bounded, flows, field, velocity, depend, exactly, nu, derivatives, force, zero.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Finite computation in a balanced zero-data fluid flow

BalancedThreeStack.lean, the release lists it as a supporting statement.

theorem balanced_three_stack_realization :    ∃ U f₀ f₁ : Family Velocity,    ∃ X : Family MaterialFlow,    ∃ repeated : FiniteMachine → Velocity,      EffectiveFamily U ∧ EffectiveFamily f₀ ∧ EffectiveFamily f₁ ∧      (∀ M, Function.Periodic (repeated M) 1) ∧      ∀ (M : FiniteMachine) (w : Input M),        Smooth (U M w) ∧ Smooth (f₀ M w) ∧ Smooth (f₁ M w) ∧        f₀ M w = inertialCoefficient (U M w) ∧        f₁ M w = viscousCoefficient (U M w) ∧        CommonCompactSupport (U M w) (f₀ M w) (f₁ M w) ∧        BoundedMixed (U M w) ∧        PeriodicAfterOne (U M w) ∧        (∀ t, 1 ≤ t → ∀ x, U M w t x = repeated M t x) ∧        ComparisonClass (U M w) (fun _ _ => 0) ∧        IsMaterialFlow (U M w) (X M w) ∧

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

NavierStokesAlternating

The paper states

Theorem 1.1

In Velocity-Field Detection of Computation in Forced Navier–Stokes Flows, 27 September 2026

For each positive computable \nu, a machine and a finite input effectively determine each of the following two forces.

  1. 1.

    On \T^3, a smooth force has a unique global smooth solution in the torus class above, with pressure zero, for which (2) holds exactly when the machine halts. The force is supported in K\times\T for a compact K\subset(0,1)^2 independent of time. Its derivatives are bounded on every finite time interval; their bounds may grow with that interval.

  2. 2.

    On \R^2\times\T, a smooth force and all its mixed derivatives are globally bounded. On each finite time interval its horizontal support is compact. It has a unique global smooth solution in (4), with pressure zero and integrable nonnegative third component. Event (3) holds exactly when the machine halts.

The sets and thresholds in both observations are independent of the machine and input. The compact set K in the first construction may depend on that instance, but is independent of time. Both force prescriptions install all the required local instructions, without executing the selected computation.

The words they share: instructions, observations, compact, supported, input, computable, machine, pressure, mixed, time, smooth, halts, force, stokes, navier, field, velocity, construction, positive, unique, finite, derivatives.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Rapidly decaying alternating-coordinate memory

NavierStokesAlternating.lean, the release lists it as a supporting statement.

theorem alternating (ν : ℝ) (hν : 0 < ν) (hc : ComputableReal ν) :    AlternatingConclusion ν := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

NavierStokesVelocity

The paper states

Theorem 1.1

In Velocity-Field Detection of Computation in Forced Navier–Stokes Flows, 27 September 2026

For each positive computable \nu, a machine and a finite input effectively determine each of the following two forces.

  1. 1.

    On \T^3, a smooth force has a unique global smooth solution in the torus class above, with pressure zero, for which (2) holds exactly when the machine halts. The force is supported in K\times\T for a compact K\subset(0,1)^2 independent of time. Its derivatives are bounded on every finite time interval; their bounds may grow with that interval.

  2. 2.

    On \R^2\times\T, a smooth force and all its mixed derivatives are globally bounded. On each finite time interval its horizontal support is compact. It has a unique global smooth solution in (4), with pressure zero and integrable nonnegative third component. Event (3) holds exactly when the machine halts.

The sets and thresholds in both observations are independent of the machine and input. The compact set K in the first construction may depend on that instance, but is independent of time. Both force prescriptions install all the required local instructions, without executing the selected computation.

The words they share: horizontal, plane, observations, integrable, eq, two, comparison, compact, event, torus, input, computable, machine, pressure, mixed, time, smooth, derivatives, bounded, force, zero, stokes, navier, field, velocity, nonnegative, positive, times, halts.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Pointwise and integral velocity-field detection of halting

NavierStokesVelocity.lean, the release lists it as a supporting statement.

theorem main_result :    ∃ B : ℕ, 0 < B ∧      (∀ s : ℝ, |deriv (deriv SmoothBump.profile) s| ≤ (B:ℝ)) ∧    ∀ (ν : ℝ), 0 < ν → ComputableReal ν →    ∀ (b N : ℕ) [NeZero b] [NeZero N]      (M : TM0.Machine (Fin b) (Fin N)) (w : List (Fin b)),    ∃ (Ftor Fcyl : ℝ → VectorField 3),      (compile B M w).Represents .torus Ftor ∧      (compile B M w).Represents .cylinder Fcyl ∧      (ContDiff ℝ ∞ (uncurry (Ftor ν)) ∧        (∀ t, FactorsThrough (Ftor ν t) PeriodicSpace.cover) ∧        (∃ K : Set (Coord 2), IsCompact K ∧ (∀ X ∈ K, ∀ i, X i ∈ Ioo (0:ℝ) 1) ∧          ∀ t X, PeriodicSpace.cover (horizontal X) ∉ PeriodicSpace.cover '' K → Ftor ν t X = 0) ∧        (∀ T d, ∃ C : ℝ, 0 ≤ C ∧ ∀ t ∈ Icc (0:ℝ) T, ∀ X,          ‖iteratedFDeriv ℝ d (uncurry (Ftor ν)) (t,X)‖ ≤ C) ∧        ∃ u : VectorField 3,

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

SolenoidalSheetPrograms

The paper states

Theorem 5.1 (Periodic lattice memory)

In Computation under Rapidly Vanishing Navier–Stokes Forcing, 27 September 2026

Fix a computable viscosity \nu>0. A finite deterministic machine and a finite input effectively determine a smooth force g on the unit flat torus \T^3=(\R/\mathbb Z)^3 with zero spatial mean. The Navier–Stokes equations with force g and zero initial velocity have a smooth solution (U,0) with zero spatial mean. Its particle from

a_*=(1/4,1/2,1/2)

enters the fixed open set

O=\{x\in\T^3:1/2<x_1<1\pmod 1\}

at some finite time if and only if the machine halts on that input. For every pair of nonnegative integers r,J and every spatial multi-index \alpha, there is an effective constant C_{r,\alpha,J} such that

\|\partial_t^r\partial_x^\alpha U(t)\|_\infty +\|\partial_t^r\partial_x^\alpha g(t)\|_\infty \le C_{r,\alpha,J}(1+t)^{-J},\qquad t\ge0.

There is also an effective smooth mean-zero solenoidal force f with the same bounds and exactly the same velocity and material event. It is f=g-\nabla\phi, with pressure -\phi, where \phi is the mean-zero periodic solution of \Delta\phi=\operatorname{div}g.

For either force, uniqueness holds among periodic classical solutions for which the velocity, its time derivative and its spatial derivatives through order two, and the pressure and its spatial gradient, are continuous on every [0,T]\times\T^3. Pressure is normalized to have zero spatial mean.

The words they share: among, bounds, computable, derivative, derivatives, effective, enters, exactly, finite, fixed, flat, force, halts, holds, input, machine, material, mean, memory, navier, nonnegative, open, particle, periodic, pressure, smooth, solenoidal, solution, solutions, spatial, stokes, time, torus, uniqueness, unit, velocity, viscosity, zero.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Positive diagonal programs on incompressible coding sheets

SolenoidalSheetPrograms.lean, the release lists it as a supporting statement.

theorem sheet_theorem {N : ℕ} (D : SheetData N) (ν : ℝ)    (hν : 0 < ν) (hνcomp : ComputableReal ν) :    ∃ f u : Field, ∃ X : ℝ → Space → Space,      SpatiallyPeriodic f ∧ SpatiallyPeriodic u ∧      Smooth f ∧ Smooth u ∧ Effective f ∧      MeanZero f ∧ DivergenceFree f ∧ OnePeriodic f ∧      ClassicalSolution ν f u (fun _ _ => 0) ∧      (∀ v : Field, ∀ p : Pressure, ClassicalSolution ν f v p →        ∀ t, 0 ≤ t → ∀ x, v t x = u t x ∧ p t x = 0) ∧      MaterialFlow u X ∧      (∀ i : Fin N, ∀ y ∈ (D.source i).carrier,        toTorus (X 1 (sheet y)) =          toTorus (sheet (diagonalMap (D.source i) (D.target i) (D.ratio i) y))) ∧      IntegerCollars u ∧ (∀ t x, advection u t x = 0) ∧      EffectiveBounds f ∧ EffectiveBounds u ∧      (N = 0 → f = 0 ∧ u = 0) := by

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).

Their note: NavierStokesAlternating.alternating (fixed computable ν > 0) gives computable compilers (Machine × input ↦ triple of Nat.Partrec.Code programs returning approximations, moduli and rapid-decay bounds) and, for every well-formed Turing machine and input, a smooth force f = residual ν U supported in one compact K, with U the unique energy-class solution from rest (zero pressure), such that the machine halts iff the particle started at (-1,0,0) reaches {x₁ > 0}. ForcedNavierStokesComputation and BalancedThreeStack (one theorem stated twice: all ν > 0, particle from (4,0,0) into (-1,2)³) and NavierStokesVelocity (torus and ℝ²×𝕋 detection) are variants. The forcing is not unconstrained: it must be uniformly computable in (M, w) (ProgramFor/EffectiveFamily/Represents), which excludes a force that already knows the halting answer.

Definitions the group asks readers to compare with the paper: The flow is prescribed and the force is derived from it: f = residual ν U := ∂ₜU + U·∇U - νΔU (Alternating) or f₀ := inertialCoefficient U, f₁ := viscousCoefficient U, affineForce f₀ f₁ ν with pressure ≡ 0 (Forced/BalancedThreeStack); legitimate for forced Navier-Stokes since solutions are shown unique in an energy comparison class, but it means the force is only constrained through smoothness, compact support, computability and uniqueness; NavierStokesVelocity: def compile (B) (M) (w) : Program b N := ⟨B, M, w⟩ is trivial packaging; the effectiveness is carried by the fixed interpreter evaluate := Nat.rfindOpt (valueTrial..) and the clause Represents, i.e. ‘terminating compiler’ there means the interpreter always halts with an ε-approximation (the genuinely computable compiler is Computable compileForce in NavierStokesAlternating); Three different machine models: Machine := ℕ × ℕ × ℕ × List ℕ × List (Option Rule) (Alternating), FiniteMachine with Option Transition (Forced/BalancedThreeStack), Mathlib Turing.TM0.Machine (Velocity), and 'halts’ is ∃ n, isHalting (run n), Halts (reachable configuration without a transition) and (TM0.eval M w).Dom respectively; BalancedThreeStack and ForcedNavierStokesComputation share the theorem name OAI.BalancedTransport.balanced_three_stack_realization and differ only by a Fintype Direction instance

“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).

“MATCHES”, in their words: The challenge statements state the headline as OpenAI wrote it.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

The formalization realizes finite families of prescribed positive diagonal maps on coding sheets by smooth incompressible flows on a flat three-torus. At every positive computable viscosity, it supplies a solution starting from rest with zero pressure and a force that is divergence free, has spatial mean zero, and is one-periodic from time zero. Each map acts on every point of its source sheet, and the construction provides effective bounds for all mixed derivatives.

This selected statement covers the sheet programs. The paper’s fixed-particle halting detector and its reciprocal maps on solid boxes are outside its scope. The formalization proves that a fluid particle can detect arbitrary finite-machine halting using alternating-coordinate memory in smooth incompressible Navier–Stokes flows whose velocity and force decay faster than every inverse power of time, including every mixed derivative. For each fixed positive computable viscosity, the construction starts from rest and provides effective forces, unique material trajectories, and an exact equivalence between entering a fixed open detector and halting. The velocity and force share one compact support for every machine and input. The solution-uniqueness assertion uses the stated energy comparison class. The formalization constructs smooth forced three-dimensional Navier–Stokes flows from rest whose velocity fields detect whether a prescribed machine halts, at any positive computable viscosity. On the unit flat torus, halting is equivalent to the vertical velocity exceeding $1/2$ somewhere in a fixed observation strip. On $\mathbb R^2\times\mathbb T$, it is equivalent to the integral of the nonnegative vertical velocity over the observation half-plane times the circle exceeding $1/2$. The torus force is confined to a fixed horizontal region. The cylindrical force has globally bounded mixed derivatives and compact horizontal support on every finite time interval. Both constructions have effective descriptions and uniqueness within their respective smooth solution-comparison classes. The formalization realizes finitely many positive diagonal affine maps of determinant one between rational solid boxes by a smooth compactly supported divergence-free flow. Source boxes are pairwise disjoint and target boxes are pairwise disjoint, while overlap between the two families is allowed. Each map holds on a neighborhood of the entire source box, and the velocity is supported in the middle half of the time interval. It also encodes every finite machine and input in a smooth, compactly supported incompressible Navier–Stokes flow on $\mathbb R^3$ starting from rest: the particle initially at $(4,0,0)$ enters the fixed open box $(-1,2)^3$ exactly when the machine halts. One velocity works for every viscosity $\nu>0$, with zero pressure and force $f_0+\nu f_1$. Velocity and force have bounded mixed derivatives and are one-periodic after time one; the repeated velocity depends only on the machine. The force is computable for computable $\nu$. Velocity is unique among smooth zero-data solutions with $u\in C_tH_x^2\cap C_t^1L_x^2$, bounded $u$ and $\nabla u$ on finite time intervals, and pressure modulo a function of time in $C_tH_x^1$.

AI-drafted comparisons, with no recorded human review

  • Effective finite computation detected by a fixed particle ForcedNavierStokesComputation

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the same balanced three-stack theorem as BalancedThreeStack: the two challenge files name the same theorem and library module and differ only in namespace layout and one instance declaration.

  • Incompressible transport of solid boxes BalancedBoxRouting

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the box-transport theorem of the current edition: finitely many diagonal affine maps of determinant one between rational boxes realised by one smooth compactly supported divergence-free flow.

  • Finite computation in a balanced zero-data fluid flow BalancedThreeStack

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the balanced three-stack theorem: every machine and input is encoded in a smooth zero-data Navier–Stokes flow on R³ in which a fixed particle enters a fixed box exactly when the machine halts.

  • Rapidly decaying alternating-coordinate memory NavierStokesAlternating

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the rapid-decay paper’s theorem on alternating memories: a fluid particle detects halting in Navier–Stokes flows whose velocity and force decay faster than every inverse power of time.

  • Pointwise and integral velocity-field detection of halting NavierStokesVelocity

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the velocity-detection paper: on the torus and on R² × T, halting is equivalent to a stated velocity threshold in a fixed observation region.

  • Positive diagonal programs on incompressible coding sheets SolenoidalSheetPrograms

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s sheet theorem: finite families of positive diagonal maps on coding sheets realised by smooth incompressible flows on the three-torus. The paper’s periodic-initialisation theorem with its fixed-particle halting detector is outside it.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Effective finite computation detected by a fixed particle ForcedNavierStokesComputation

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Incompressible transport of solid boxes BalancedBoxRouting

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 125 s; peak memory 6.2 GiB).10 October 2026Original report

Finite computation in a balanced zero-data fluid flow BalancedThreeStack

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Rapidly decaying alternating-coordinate memory NavierStokesAlternating

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 131 s; peak memory 6.3 GiB).11 October 2026Original report

Pointwise and integral velocity-field detection of halting NavierStokesVelocity

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Positive diagonal programs on incompressible coding sheets SolenoidalSheetPrograms

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 162 s; peak memory 6.4 GiB).10 October 2026Original report

Explanations by others

Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.

  • seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source

    Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

Follow-up work by others

  • From community.openai.com, 6 October 2026. Source

    zussini proposes correcting 12 stale manuscript references in five Lean files of the separate NavierStokesAndEuler repository; the audited commit is f9e8bc5b; issues and pull requests are disabled there.

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare one Lean statement with its paper: SolenoidalSheetPrograms, NavierStokesAlternating, NavierStokesVelocity, BalancedBoxRouting, BalancedThreeStack, ForcedNavierStokesComputationSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a construction and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.

    Author not stated. Source

  • From github.com/jkbennitt/math-release-atlas, 9 October 2026. Source

    The math-release-atlas shows a fixed caution on this family: it is a forced Navier-Stokes computation and not the Clay Millennium Navier-Stokes problem.

  • Peter Woit, Slopocalypse, 6 October 2026. Source

    Cites arXiv 2610.08144 (Bastounis, Circelli, Hansen) as grounds to doubt Lean certification of the Navier-Stokes blow-up statement.

  • Terence Tao, Navier-Stokes as a worked example of AI solutions contaminating a field, 5 September 2026. Source

    5 Sep clarification says they were not aware of any significant Navier-Stokes development and that the discussion was hypothetical.

  • Terence Tao, Navier-Stokes as a worked example of AI solutions contaminating a field, 3 September 2026. Source

    Post 3/3 of 3 Sep says three AI companies raced to announce bounded-gaps improvements the same day and that Stadlmann’s human preprint escaped contamination just in time.

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 376 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 376 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form