{"id":"arxiv/2607.08986","url":"https://arxiv.org/abs/2607.08986","tags":["cs.AI","cs.LO","math-ph","math.AP"],"score":0,"title":"A Formalization of the Mean-Field Derivation of the Vlasov Equation","domain":"cs.AI","source":"arxiv","authors":["Joseph K. Miller"],"reviews":0,"subject":"cs.AI","summary":"We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game. The objective is to turn a LaTeX document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone. Reuse is a second check, by a definition we introduce: whether the development yields a self-contained layer of general mathematics the wider library could absorb. The case study is a complete, axiom-clean formalization of…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-09","reactions":{}}