This blueprint is a reader’s map of a Lean 4 / Mathlib formalization of the mean-field derivation of the Vlasov equation: forward well-posedness, Dobrushin’s 1979 stability estimate, the mean-field limit, and a short-window superposition principle (weak solutions are Lagrangian). The statements on the cards below are extracted from the elaborated Lean proof terms, and the edges of the dependency graph are computed from the proofs themselves, not asserted. Where a card corresponds to a numbered statement of the companion paper, the paper’s number appears in its title. The three apex theorems — well-posedness, Dobrushin stability, and the superposition principle — each carry the axiom footprint \([\mathtt{propext}, \mathtt{Classical.choice}, \mathtt{Quot.sound}]\): Lean’s three standard axioms, no sorry, no project-specific axioms.

Companion artifacts: the paper (A Formalization of the Mean-Field Derivation of the Vlasov Equation), the repository, and the API documentation — every declaration, searchable, with source links to the exact commit. Each card’s “Lean declarations” button resolves to its API page.