OpenAI claim summary for Math-2219

Vlasov–Maxwell regularity

OpenAI's claim

Relativistic Vlasov--Maxwell regularity: The paper claims global classical well-posedness of the relativistic Vlasov--Maxwell equations in three dimensions for a single particle species with arbitrary admissible smooth data of the specified finite-energy and particle-support class. Neither smallness nor symmetry is required.

Mathematical statement of the claimed result

Mathematical claim 1.

Let $u(v)=v/\sqrt{1+|v|^2}$, $\rho=\int f\,dv$, $j=\int u(v)f\,dv$. The system is \[\begin{aligned}\partial_tf+u\cdot\nabla_xf+(E+u\times B)\cdot\nabla_vf&=0,\\\partial_tE-\nabla\times B&=-j,&\partial_tB+\nabla\times E&=0,\\\nabla\cdot E&=\rho,&\nabla\cdot B&=0.\end{aligned}\] For arbitrary nonnegative $f_0\in C_c^\infty(\mathbb R_x^3\times\mathbb R_v^3)$ and $E_0,B_0\in C_b^\infty\cap L^2(\mathbb R^3;\mathbb R^3)$ satisfying the divergence constraints, the claim gives a unique global classical solution, smooth on every finite time interval, with compact phase-space support for $f$ on each such interval. Uniqueness refers to $C^1$ pointwise solutions with $E,B\in C([0,\infty);L^2(\mathbb R^3;\mathbb R^3))$ and one compact phase-space support set for $f$ over each bounded time interval. The data class $C_b^\infty$ requires every spatial derivative bounded. No smallness or symmetry is assumed, but compact support of the initial particle density is required.

Outline of the argument

Relativistic Vlasov--Maxwell regularity: The key quantity is the vector impulse integrated along a particle characteristic, with its norm taken after the integration. Retarded-field formulas, occupation estimates, and signed cancellation bound the time needed for successive momentum doublings. The lower bounds have divergent total length, so particle momentum support cannot blow up in finite time and the continuation criterion closes.

Formal verification

Family 362 describes Lean coverage for global smooth one-species relativistic Vlasov--Maxwell evolution for the stated admissible data class.

Relativistic Vlasov--Maxwell regularity: The manuscript links VlasovMaxwell.lean (declaration OAI.RVM.global_classical_solution).

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, Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system, 2026-09-23; citation key OAI:Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:global.
• Family 362: Lean scope.
• Comparator VlasovMaxwell.json.
• Comparator VlasovMaxwell.lean.
• Family 362: Reasoning summary.
• OpenAI catalogue entry.