OpenAI claims global smoothness for 3D relativistic Vlasov–Maxwell (Lean)

Your AI and this story

Key facts

• Claim (abstract, verbatim): ‘We prove global existence and uniqueness for arbitrary smooth admissible initial data in the three-dimensional, one-species relativistic Vlasov–Maxwell system. … This resolves the large-data global classical regularity problem for this model, without size or symmetry restrictions on the data.’
• Earlier results, as the paper recounts them: Wollman’s local classical theory; global weak solutions (DiPerna–Lions; Rein); Glassey and Strauss’s bounded-momentum continuation criterion and global existence for dilute plasmas; lower-dimensional reductions (Glassey–Schaeffer); small-data and small-particle results (Schaeffer, Bigorgne, Wang, Wei–Yang); Xuecheng Wang’s large-data result for cylindrically symmetric data, which the paper dates to a ‘July 2026 two-paper treatment’. The paper: ‘These results use restrictions on size, dimension, or the reference configuration’
• Mechanism (paper §1.2): ‘The central estimate concerns the signed change of a particle’s momentum … We take the norm after integration.’ Lower bounds on the time needed to double the largest momentum ‘have a divergent sum, which rules out unbounded momentum support in finite time’. Absolute force bounds lose a factor √w; this loss is removed by integrating the retarded force by parts along source trajectories in a narrow angular sector
• Lean: comparator challenge VlasovMaxwell.lean (OAI.RVM.global_classical_solution) writes out the Vlasov, Maxwell and Gauss equations and the class of admissible data, and asserts uniqueness among C¹ solutions with compact phase support. Scope note: ‘No smallness, symmetry, or neutrality assumption is imposed.’ Accepted in the oai-math-revised comparator run of 25–26 Oct (‘Lean default kernel accepts the solution’); MathVet verdict ‘full’, with a sandboxed pass. Ying Xie counts 207 Lean files
• OpenAI’s reasoning summary (one of ten published) ends: ‘The assistant ended by asserting global smooth continuation. That assertion rests on the occupation bound, direction-count estimate, and cutoff cancellations needed to close the signed momentum bootstrap; the cited continuation theorem alone does not establish those estimates.’
• Caveats from Ying Xie’s survey (arXiv 2610.17090, 12 Oct): Cheverry–Ibrahim’s work is ‘cited six times in the summary and omitted from the paper’; ‘The exponent comparison has a small margin’ (an exponent contradiction, 0.496z against 0.41z); ‘Uniqueness is asserted only among global classical solutions’
• Trackers: AIM problem 073 is marked SOLVED (13 Oct). Its maintainer, Matthew Colbrook, wrote on PR #35 that the comparator file ‘is a statement, not a checked proof … we keep Solved from the published manuscript and do not claim Lean-verified status. This is not a finding that the manuscript is only partial.’ On 29 Oct Wikipedia’s list of unsolved problems still included ‘Regularity of solutions of Vlasov–Maxwell equations’
• Reactions: none from kinetic theorists found as of 29 Oct. We searched the web, arXiv, Hacker News and Proofs and Prompts; the oai-math-revised notes report ‘Follow-up works: None found’. The same notes cite a Reddit commenter who says they work in the area and found that nonstandard notation made the central idea hard to identify; we could not open the comment