Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Incompressible transport of solid boxes

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.BoxTransport.Routing.balanced_box_routing

Lean statement file: BalancedBoxRouting.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 376 link it.

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

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

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

  • abbreviation OAI.BoxTransport.Routing.Space line 9

    abbrev Space := Fin 3 → ℝ
  • abbreviation OAI.BoxTransport.Routing.RationalSpace line 10

    abbrev RationalSpace := Fin 3 → ℚ
  • abbreviation OAI.BoxTransport.Routing.SpaceTime line 11

    abbrev SpaceTime := ℝ × Space
  • abbreviation OAI.BoxTransport.Routing.Field line 13

    abbrev Field := SpaceTime → Space
  • abbreviation OAI.BoxTransport.Routing.Axis line 15

    abbrev Axis := Option (Fin 3)
  • definition OAI.BoxTransport.Routing.coordinateVector line 17

    def coordinateVector (j : Fin 3) : Space := Pi.single j 1
  • definition OAI.BoxTransport.Routing.coordinateDirection line 19

    def coordinateDirection : Axis → SpaceTime  | none => (1, 0)  | some j => (0, coordinateVector j)
  • definition OAI.BoxTransport.Routing.realPoint line 23

    def realPoint (q : RationalSpace) : Space := fun j => (q j : ℝ)
  • definition OAI.BoxTransport.Routing.realBox line 27

    def realBox (c r : Space) : Set Space :=  {x | ∀ j, |x j - c j| ≤ r j}
  • definition OAI.BoxTransport.Routing.solidBox line 30

    def solidBox (a h : RationalSpace) : Set Space :=  realBox (realPoint a) (realPoint h)
  • definition OAI.BoxTransport.Routing.prescribedAffine line 33

    def prescribedAffine (a b h k : RationalSpace) (x : Space) : Space :=  fun j => (b j : ℝ) + ((k j / h j : ℚ) : ℝ) * (x j - (a j : ℝ))
  • definition OAI.BoxTransport.Routing.mixedDerivative line 36

    noncomputable def mixedDerivative : List Axis → Field → Field  | [], U => U  | j :: js, U => fun p => fderiv ℝ (mixedDerivative js U) p (coordinateDirection j)
  • abbreviation OAI.BoxTransport.Routing.RationalCode line 40

    abbrev RationalCode := ℕ × ℕ × ℕ
  • definition OAI.BoxTransport.Routing.rationalValue line 42

    def rationalValue (q : RationalCode) : ℚ := ((q.1 : ℚ) - q.2.1) / (q.2.2 + 1)
  • abbreviation OAI.BoxTransport.Routing.RationalPointCode line 44

    abbrev RationalPointCode := RationalCode × RationalCode × RationalCode × RationalCode
  • definition OAI.BoxTransport.Routing.codeSpaceTime line 46

    def codeSpaceTime (q : RationalPointCode) : SpaceTime :=  ((rationalValue q.1 : ℝ), ![(rationalValue q.2.1 : ℝ),    (rationalValue q.2.2.1 : ℝ), (rationalValue q.2.2.2 : ℝ)])
  • abbreviation OAI.BoxTransport.Routing.EvaluationRequest line 50

    abbrev EvaluationRequest := List Axis × RationalPointCode × ℕ × Fin 3
  • definition OAI.BoxTransport.Routing.Effective line 52

    def Effective (U : Field) : Prop :=
    Show the remaining 11 lines
      ∃ eval : EvaluationRequest → RationalCode,    ∃ modulus : List Axis × ℕ → ℕ,      ∃ bound : List Axis → ℕ,        Computable eval ∧ Computable modulus ∧ Computable bound ∧        (∀ (ds : List Axis) (q : RationalPointCode) (n : ℕ) (p : SpaceTime),          ‖p - codeSpaceTime q‖ ≤ ((modulus (ds, n) : ℝ) + 1)⁻¹ →          ∀ j : Fin 3,            |mixedDerivative ds U p j - (rationalValue (eval (ds, q, n, j)) : ℝ)| ≤              ((n : ℝ) + 1)⁻¹) ∧        (∀ (ds : List Axis) (p : SpaceTime) (j : Fin 3),          |mixedDerivative ds U p j| ≤ (bound ds : ℝ))
  • definition OAI.BoxTransport.Routing.spatialDivergence line 65

    noncomputable def spatialDivergence (U : Field) (t : ℝ) (x : Space) : ℝ :=  ∑ j : Fin 3, (fderiv ℝ (fun y => U (t, y)) x (coordinateVector j)) j
  • definition OAI.BoxTransport.Routing.AdmissibleField line 68

    def AdmissibleField (U : Field) : Prop :=  ContDiff ℝ ∞ U ∧ HasCompactSupport U ∧ Effective U ∧    (∀ t x, spatialDivergence U t x = 0) ∧    (∀ (t : ℝ) (x : Space), t ∉ Set.Icc (1 / 4 : ℝ) (3 / 4 : ℝ) → U (t, x) = 0)
  • definition OAI.BoxTransport.Routing.IsGlobalFlow line 73

    def IsGlobalFlow (U : Field) (Φ : ℝ → Space → Space) : Prop :=  (∀ x, Φ 0 x = x) ∧    (∀ t x, HasDerivAt (fun s => Φ s x) (U (t, Φ t x)) t) ∧    (∀ (x : Space) (γ : ℝ → Space), γ 0 = x →      (∀ t, HasDerivAt γ (U (t, γ t)) t) → ∀ t, γ t = Φ t x)
  • definition OAI.BoxTransport.Routing.Delivers line 79

    def Delivers {n : ℕ} (a b h k : Fin n → RationalSpace)    (Φ : ℝ → Space → Space) : Prop :=  ∀ i, ∃ O : Set Space, IsOpen O ∧ solidBox (a i) (h i) ⊆ O ∧    ∀ x ∈ O, Φ 1 x = prescribedAffine (a i) (b i) (h i) (k i) x

No confident match with a paper statement

No paper theorem is paired with this Lean statement.

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

Statements in Incompressible Box Transport and Finite Computation come first because the release’s name for this Lean statement shares words with that paper’s title.

Other possible paper matches, closest wording first

  • Proposition 13.5 of Incompressible Box Transport and Finite Computation. Words of the Lean statement, its names split into words, that also appear in the theorem: axis, solid, pairwise, point, affine, disjoint and eight more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: entire, source, target, families, half, map and three more.
  • Proposition 13.1 of Incompressible Box Transport and Finite Computation. Words of the Lean statement, its names split into words, that also appear in the theorem: axis, pairwise, point, affine, disjoint, rational and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: determinant, diagonal, transport, families, map, compactly and two more.
  • Theorem 3.4 of Incompressible Box Transport and Finite Computation. Words of the Lean statement, its names split into words, that also appear in the theorem: js, solid, pairwise, disjoint, 3/4, rational and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: half, family, neighborhood, map, compactly, interval and three more.
  • Proposition 13.7 of Incompressible Box Transport and Finite Computation. Words of the Lean statement, its names split into words, that also appear in the theorem: values, affine, disjoint, rational, coordinate, field and five more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: diagonal, transport, families, maps, positive and realizes.
  • Proposition 13.3 of Incompressible Box Transport and Finite Computation. Words of the Lean statement, its names split into words, that also appear in the theorem: point, disjoint, coordinates, box, integer, effective and one more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: transported, source, target, families, maps and positive.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

three independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet; Neal McBurnett’s openai-math-lean-tooling. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

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

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

  • Accepted Their term: “CERTIFIED”.

    Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.

    Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

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. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Accepted Their term: “comparator-sandboxed-pass”.

    Re-run through Comparator in a sandboxed virtual machine: accepted.

    Reported 8 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

  • Accepted Their term: “accepted”.

    Re-run through Comparator with Lean’s kernel: accepted (the check took 125 s; peak memory 6.2 GiB).

    Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 376’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

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

  • MathVet

    Finds the whole advertised result stated or implied Their term: “full”.

    The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record

    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

  • Carlos Toledo’s cert-machine

    Finds the whole advertised result stated or implied Their term: “MATCHES”.

    The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

96 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 84 to its own declarations, 38 to Mathlib’s documentation. 24 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAIopen scoped BigOperators ContDiffnamespace BoxTransport.Routingabbrev Space := Fin 3 → ℝabbrev RationalSpace := Fin 3 → ℚabbrev SpaceTime := ℝ × Spaceabbrev RationalSpaceTime := ℚ × RationalSpaceabbrev Field := SpaceTime → Spaceabbrev Axis := Option (Fin 3)def coordinateVector (j : Fin 3) : Space := Pi.single j 1def coordinateDirection : Axis → SpaceTime  | none => (1, 0)  | some j => (0, coordinateVector j)def realPoint (q : RationalSpace) : Space := fun j => (q j : ℝ)def realSpaceTime (q : RationalSpaceTime) : SpaceTime := (q.1, realPoint q.2)def realBox (c r : Space) : Set Space :=  {x | ∀ j, |x j - c j| ≤ r j}def solidBox (a h : RationalSpace) : Set Space :=  realBox (realPoint a) (realPoint h)def prescribedAffine (a b h k : RationalSpace) (x : Space) : Space :=  fun j => (b j : ℝ) + ((k j / h j : ℚ) : ℝ) * (x j - (a j : ℝ))noncomputable def mixedDerivative : List Axis → Field → Field  | [], U => U  | j :: js, U => fun p => fderiv ℝ (mixedDerivative js U) p (coordinateDirection j)abbrev RationalCode := ℕ × ℕ × ℕdef rationalValue (q : RationalCode) : ℚ := ((q.1 : ℚ) - q.2.1) / (q.2.2 + 1)abbrev RationalPointCode := RationalCode × RationalCode × RationalCode × RationalCodedef codeSpaceTime (q : RationalPointCode) : SpaceTime :=  ((rationalValue q.1 : ℝ), ![(rationalValue q.2.1 : ℝ),    (rationalValue q.2.2.1 : ℝ), (rationalValue q.2.2.2 : ℝ)])abbrev EvaluationRequest := List Axis × RationalPointCode × ℕ × Fin 3def Effective (U : Field) : Prop :=  ∃ eval : EvaluationRequest → RationalCode,    ∃ modulus : List Axis × ℕ → ℕ,      ∃ bound : List Axis → ℕ,        Computable eval ∧ Computable modulus ∧ Computable bound ∧        (∀ (ds : List Axis) (q : RationalPointCode) (n : ℕ) (p : SpaceTime),          ‖p - codeSpaceTime q‖ ≤ ((modulus (ds, n) : ℝ) + 1)⁻¹ →          ∀ j : Fin 3,            |mixedDerivative ds U p j - (rationalValue (eval (ds, q, n, j)) : ℝ)| ≤              ((n : ℝ) + 1)⁻¹) ∧        (∀ (ds : List Axis) (p : SpaceTime) (j : Fin 3),          |mixedDerivative ds U p j| ≤ (bound ds : ℝ))noncomputable def spatialDivergence (U : Field) (t : ℝ) (x : Space) : ℝ :=  ∑ j : Fin 3, (fderiv ℝ (fun y => U (t, y)) x (coordinateVector j)) jdef AdmissibleField (U : Field) : Prop :=  ContDiff ℝ ∞ U ∧ HasCompactSupport U ∧ Effective U ∧    (∀ t x, spatialDivergence U t x = 0) ∧    (∀ (t : ℝ) (x : Space), t ∉ Set.Icc (1 / 4 : ℝ) (3 / 4 : ℝ) → U (t, x) = 0)def IsGlobalFlow (U : Field) (Φ : ℝ → Space → Space) : Prop :=  (∀ x, Φ 0 x = x) ∧    (∀ t x, HasDerivAt (fun s => Φ s x) (U (t, Φ t x)) t) ∧    (∀ (x : Space) (γ : ℝ → Space), γ 0 = x →      (∀ t, HasDerivAt γ (U (t, γ t)) t) → ∀ t, γ t = Φ t x)def Delivers {n : ℕ} (a b h k : Fin n → RationalSpace)    (Φ : ℝ → Space → Space) : Prop :=  ∀ i, ∃ O : Set Space, IsOpen O ∧ solidBox (a i) (h i) ⊆ O ∧    ∀ x ∈ O, Φ 1 x = prescribedAffine (a i) (b i) (h i) (k i) xtheorem 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  sorryend BoxTransport.Routingend OAI
Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Geometric Programs for Solenoidal Forcing

Theorem (Periodic initialization)

Fix a computable viscosity \nu>0. From a deterministic one-tape machine, with head moves in \{-1,0,1\}, and a finite input, one can effectively construct a smooth force on \mathbb T_1^3 such that:

  1. (i)

    The force is divergence free, has zero spatial mean, and is one-periodic from time zero. Equation (sv:NS) has a global smooth solution with pressure zero, unique in the stated classical class.

  2. (ii)

    The velocity is one-periodic, vanishes near every integer time, has zero instantaneous self-advection, and has uniformly bounded kinetic energy. Every mixed derivative of force and velocity is globally bounded.

  3. (iii)

    For the fixed label a_*=(1/4,1/2,1/4) and fixed open strip O=\{1/2<x_1<7/8\}, the material trajectory enters O at a finite real time exactly when the machine halts, including an initially halted machine.

The construction may use one Cartesian velocity component at a time. For arbitrary fixed real \nu>0 the same formulas hold and are effective relative to that viscosity.

Section 1, The geometry of a finite fluid instruction Read it in the paper TeX source, line 43
Show the TeX
Fix a computable viscosity $\nu>0$.  From a deterministic one-tape
machine, with head moves in $\{-1,0,1\}$, and a finite input, one can
effectively construct a smooth force on $\mathbb T_1^3$ such that:
\begin{enumerate}[label=(\roman*),itemsep=2pt]
\item The force is divergence free, has zero spatial mean, and is
one-periodic from time zero.  Equation~\eqref{sv:NS} has a global
smooth solution with pressure zero, unique in the stated classical class.
\item The velocity is one-periodic, vanishes near every integer time,
has zero instantaneous self-advection, and has uniformly bounded kinetic
energy.  Every mixed derivative of force and velocity is globally bounded.
\item For the fixed label $a_*=(1/4,1/2,1/4)$ and fixed open strip
$O=\{1/2<x_1<7/8\}$, the material trajectory enters $O$ at a finite
real time exactly when the machine halts, including an initially halted
machine.
\end{enumerate}
The construction may use one Cartesian velocity component at a time.
For arbitrary fixed real $\nu>0$ the same formulas hold and are
effective relative to that viscosity.
Theorem (General diagonal maps on a sheet)

Let P_i,Q_i\subset[2,3]^2, 1\le i\le N, be closed rectangles with rational vertices and positive side lengths. Suppose the sources are pairwise positively separated and the targets are pairwise positively separated. Let F_i:P_i\to Q_i be the center-to-center affine map with any positive rational diagonal linear part, with F_i(P_i)=Q_i. For each computable \nu>0 there is an effective smooth mean-zero solenoidal force on \mathbb T_{10}^3, one-periodic from time zero, whose unique solution in the classical class has pressure zero and period map

(y,2)\longmapsto(F_i(y),2)\qquad(y\in P_i).

Its velocity is zero near integer times and has zero self-advection; all mixed derivatives of force and velocity are bounded. No condition is imposed on source–target intersections. For N=0 use zero.

Section 1, The geometry of a finite fluid instruction Read it in the paper TeX source, line 75
Show the TeX
Let $P_i,Q_i\subset[2,3]^2$, $1\le i\le N$, be closed rectangles
with rational vertices and positive side lengths.  Suppose the sources are pairwise
positively separated and the targets are pairwise positively separated.
Let $F_i:P_i\to Q_i$ be the center-to-center affine map with any
positive rational diagonal linear part, with $F_i(P_i)=Q_i$.  For each computable $\nu>0$
there is an effective smooth mean-zero solenoidal force on
$\mathbb T_{10}^3$, one-periodic from time zero, whose unique solution
in the classical class has pressure zero and period map
\[
 (y,2)\longmapsto(F_i(y),2)\qquad(y\in P_i).
\]
Its velocity is zero near integer times and has zero self-advection;
all mixed derivatives of force and velocity are bounded.  No condition
is imposed on source--target intersections.  For $N=0$ use zero.

Computation under Rapidly Vanishing Navier–Stokes Forcing

Theorem (Compact support and rapid decay)

Fix a positive computable viscosity \nu. From a deterministic Turing machine M and a finite input w one can effectively construct a smooth force on [0,\infty)\times\R^3, supported for all times in the fixed compact set

K=[-2,1]\times[-1,2]\times[-1,1],

such that, for every pair of nonnegative integers J,l and spatial multi-index \alpha,

\sup_{t\geq0,\,x\in\R^3} (1+t)^J\bigl|\partial_t^l\partial_x^\alpha f(t,x)\bigr|<\infty.

The Navier–Stokes equation with this force and zero initial velocity has an explicit global smooth solution, unique in the finite-interval class (eq:energy-class). Its material trajectory from the origin satisfies

M\text{ halts on }w \quad\Longleftrightarrow\quad X_1(t,0)<-1\text{ for some }t\geq0.

The velocity has the same fixed support and rapid mixed-derivative bounds. The pressure is zero. The force is a general body force. Because K is fixed, the same bounds hold with (1+t+|x|)^J in place of (1+t)^J.

Section 3, Addressed compact curls Read it in the paper TeX source, line 11
Show the TeX
Fix a positive computable viscosity $\nu$. From a deterministic Turing machine $M$ and a
finite input $w$ one can effectively construct a smooth force on
$[0,\infty)\times\R^3$, supported for all times in the fixed compact set
\[
 K=[-2,1]\times[-1,2]\times[-1,1],
\]
such that, for every pair of nonnegative integers $J,l$ and spatial
multi-index $\alpha$,
\begin{equation}
 \sup_{t\geq0,\,x\in\R^3}
 (1+t)^J\bigl|\partial_t^l\partial_x^\alpha f(t,x)\bigr|<\infty.
 
\end{equation}
The Navier--Stokes equation with this force and zero initial velocity has
an explicit global smooth solution, unique in the finite-interval class \eqref{eq:energy-class}.  Its material trajectory from
the origin satisfies
\begin{equation}
 M\text{ halts on }w
 \quad\Longleftrightarrow\quad
 X_1(t,0)<-1\text{ for some }t\geq0.
 
\end{equation}
The velocity has the same fixed support and rapid mixed-derivative bounds.
The pressure is zero. The force is a general body force. Because $K$ is fixed,
the same bounds hold with $(1+t+|x|)^J$ in place of $(1+t)^J$.
Theorem (Rapid decay with alternating memories)

Fix a positive computable viscosity. From a deterministic Turing machine and a finite input one can effectively construct a smooth force f on [0,\infty)\times\mathbb R^3, with spatial support contained in a fixed compact set independent of time, such that for every J,l\geq0 and spatial multi-index \alpha,

\sup_{t\geq0,\,X\in\mathbb R^3} (1+t+|X|)^J |\partial_t^l\partial_X^\alpha f(t,X)|<\infty.

The solution with zero initial velocity is explicit, global, and unique in the class (eq:energy-class), with pressure zero. Its velocity satisfies the same support and derivative estimates. The material particle initially at (-1,0,0) reaches X_1>0 if and only if the machine halts.

Section 4, Alternating fractional memories Read it in the paper TeX source, line 11
Show the TeX
Fix a positive computable viscosity. From a deterministic Turing machine
and a finite input one can effectively
construct a smooth force $f$ on $[0,\infty)\times\mathbb R^3$, with
spatial support contained in a fixed compact set independent of time,
such that for every $J,l\geq0$ and spatial multi-index $\alpha$,
\begin{equation}
 \sup_{t\geq0,\,X\in\mathbb R^3}
 (1+t+|X|)^J
 |\partial_t^l\partial_X^\alpha f(t,X)|<\infty.
 
\end{equation}
The solution with zero initial velocity is explicit, global, and unique
in the class \eqref{eq:energy-class}, with pressure zero.  Its velocity satisfies
the same support and derivative estimates.  The material particle
initially at $(-1,0,0)$ reaches $X_1>0$ if and only if the machine halts.
Theorem (Periodic lattice memory)

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.

Section 5, Periodic lattice memory on the torus Read it in the paper TeX source, line 18
Show the TeX
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
\begin{equation}
 \|\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.
\end{equation}
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.

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

Theorem

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 (eq:torus-event) 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 (eq:comparison-class), with pressure zero and integrable nonnegative third component. Event (eq:plane-event) 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.

Section 1, Observing the velocity rather than a particle Read it in the paper TeX source, line 98
Show the TeX
For each positive computable $\nu$, a machine and a finite input
effectively determine each of the following two forces.
\begin{enumerate}
\item On $\T^3$, a smooth force has a unique global smooth solution
in the torus class above, with pressure zero, for which
\eqref{eq:torus-event} 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.
\item 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
\eqref{eq:comparison-class}, with pressure zero and integrable
nonnegative third component. Event~\eqref{eq:plane-event} holds exactly
when the machine halts.
\end{enumerate}
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.

Incompressible Box Transport and Finite Computation

The atlas found no headline statement in this paper’s TeX source.

Configuration and file facts
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 376 link it.
Solution module
OAI.Analysis.BoxTransport.Routing
Allowed axioms
propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib
Imports from outside Mathlib
None
Local vocabulary
24 local vocabulary declarations
Lines of Lean, without comments or blank lines
64
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas

Incompressible transport of solid boxes

Family 376: Universal computation in forced Navier–Stokes flows

No paper statement selected

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

The Lean statement says

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

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

No paper theorem is paired with this Lean statement.three independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

24 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/BalancedBoxRouting.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

Compare this statement with the paperShare a Comparator run reportSuggest a change