Lean formalization in OpenAI math repository (Result 362)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system'. We prove global existence and uniqueness for arbitrary smooth admissible initial data in the three-dimensional, one-species relativistic Vlasov–Maxwell system. The particle density is initially compactly supported, and the electromagnetic fields have finite energy and bounded derivatives of all orders. The solution remains smooth on every finite time interval. This resolves the large-data global classical regularity problem for this model, without size or symmetry restrictions on the data.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 362). The Lean development was not rebuilt locally.