OpenAI claim summary for Math-2853

Computation under rapidly vanishing force in one fixed spatial box

OpenAI's claim

Computation with rapidly decaying forcing: The manuscript claims particle-based halting detection from rest with every mixed derivative of force and velocity decreasing faster than any inverse time power. Each simulated machine step can occupy one unit of physical time.

Mathematical statement of the claimed result

Mathematical claim 1.

For the incompressible system $\partial_tu+(u\cdot\nabla)u=-\nabla p+\nu\Delta u+f$, $\nabla\cdot u=0$, $u(0)=0$, choose viscosity $\nu>0$, whose value is computable. On $\mathbb R^3$, the effective force and explicit velocity are supported for all times in the fixed $K=[-2,1]\times[-1,2]\times[-1,1]$, and every mixed derivative satisfies \[\sup_{t,x}(1+t)^J|\partial_t^lD_x^\alpha f(t,x)|<\infty\quad(J,l\ge0),\] with the same bounds for $u$. Pressure is zero and the solution is unique on finite intervals in the energy class $u\in CH^2\cap C^1L^2$, bounded $u,\nabla u$, with pressure modulo constants in $CH^1$. The particle from the origin satisfies $M(w)\text{ halts}\Longleftrightarrow X_1(t,0)<-1$ at some time. The prescribed force is a general body force, not required divergence free.

Outline of the argument

Computation with rapidly decaying forcing: Three separate memories use moving curls, alternating fractional coordinates, or a periodic torus lattice. Earlier records are preserved at successively separated spatial scales while signal amplitudes shrink. Exact open detectors continue to distinguish halting, and derivative estimates account for both the shrinking gates and the retained history.

Formal verification

Family 376 describes Lean coverage for the selected sheet-program, rapidly decaying particle-detector, velocity-detector, and full-box transport statements described separately in its Comparator files.

Computation with rapidly decaying forcing: The manuscript links BalancedBoxRouting.lean, BalancedThreeStack.lean, ForcedNavierStokesComputation.lean, NavierStokesAlternating.lean, NavierStokesVelocity.lean, SolenoidalSheetPrograms.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

• OpenAI, Computation under Rapidly Vanishing Navier–Stokes Forcing, 2026-09-27; citation key OAI:Computation-under-Rapidly-Vanishing-Navier-Stokes-Forcing-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:rapid.
• Family 376: Lean scope.
• Comparator BalancedBoxRouting.json.
• Comparator BalancedBoxRouting.lean.
• Comparator BalancedThreeStack.json.
• Comparator BalancedThreeStack.lean.
• Comparator ForcedNavierStokesComputation.json.
• Comparator ForcedNavierStokesComputation.lean.
• Comparator NavierStokesAlternating.json.
• Comparator NavierStokesAlternating.lean.
• Comparator NavierStokesVelocity.json.
• Comparator NavierStokesVelocity.lean.
• Comparator SolenoidalSheetPrograms.json.
• Comparator SolenoidalSheetPrograms.lean.
• OpenAI catalogue entry.