We formalize a research result in the Lean 4 proof assistant, guided by a mathematician directing an AI system, framing the activity as a formalization game. The objective is to convert a LaTeX document into Lean code. The game is won when the development compiles, contains no errors, and a machine check confirms that the target theorems rely solely on Lean's foundational axioms. A second check we introduce is reusability: whether the development yields a self-contained layer of general mathematics that the wider library could absorb.
The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route—covering existence, uniqueness, stability estimates, mean-field limits, and a short-window superposition principle (weak solutions are Lagrangian). The human's role was to direct, not to write proofs: to scope definitions, steer decompositions, and triage gaps in the library; the AI agent executed.
The formalization certifies the proof of each statement as written; whether the written statement is the intended theorem remains the mathematician's judgment. The optimal-transport machinery that emerged from the build (notably, properties of the Wasserstein-1 metric and the Kantorovich-Rubinstein duality theorem) separates into a self-contained layer that compiles against Mathlib alone: about a sixth of the development (49 of 299 declarations), linked by a 22-declaration interface with no reverse dependency. The headline theorems ran in about a week, the full development in about a month. We report the quantitative claims as observations from one game, not as general laws. The game's rules name no particular system, so the methodological framing is meant to outlast the tools of any one run.