A Formalization of the Mean-Field Derivation of the Vlasov Equation

Joseph K. Miller

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…