An AI agent (Claude Code), directed by a mathematician, produces an axiom-clean Lean 4/Mathlib formalization of Vlasov equation well-posedness and its mean-field limit.
Abstract
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 well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route – existence, uniqueness, the stability estimate and mean-field limit, and a short-window superposition principle (weak solutions are Lagrangian). The human's role was to direct, not to write proofs: to scope the definitions, steer the decompositions, and triage the library's gaps; the AI agent executed. The formalization certifies the proof of each statement as written; whether the written statement is the intended theorem stays the mathematician's judgment. The optimal-transport machinery that fell out of the build (in particular, 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), behind 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 of 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.
Problem
AI agents can now write Lean proofs quickly. That raises two questions: whether machine-written formalizations can be trusted, and whether the code they leave behind can be reused. The authors test both on a research-level result in kinetic theory: Dobrushin's mean-field derivation of the nonlinear Vlasov equation.
Approach
Formalization is framed as a game. It is won when the Lean development compiles, contains no sorry, and #print axioms shows only propext, Classical.choice and Quot.sound. Reuse is checked separately through a 'self-contained layer' meeting four library-defined criteria: dependency isolation, a standalone build against Mathlib, linter cleanliness, and reachability from a target. A mathematician scoped the definitions and steered the decompositions, while Claude Code agents and sub-agents wrote the proofs.
Figure 1: A roadmap of the development: the project blueprint’s dependency graph, auto-extracted from the elaborated Lean proof terms — boxes are definitions, ellipses theorems, green fully formalized. The interactive version, with statements and proof sketches on every node, is at hydrodynamical.github.io/Vlasov_Meanfield_Formalization .Figure 4: From the case study of Section 3 : all 362 commits classified by primary intent. Roughly one in seven is pure meta-knowledge capture (discipline / lessons) — a direct, if heuristic, measure of the meta-learning loop, distinct from the proof work itself.
Results
The development is a complete, axiom-clean formalization of existence, uniqueness, the stability estimate, the mean-field limit and a short-window superposition principle. Its optimal-transport layer (Wasserstein-1 metric, Kantorovich–Rubinstein duality) is 49 of 299 declarations, sits behind a 22-declaration interface, and compiles against Mathlib alone. The headline theorems took about a week and the full development about a month, over 362 commits.
Figure 2: From the case study of Section 3 ( 362 commits): live sorry count per production file, stacked so the leaves sum to the total (black line). The open-goal front is concentrated in one active leaf at a time and migrates across the development; the total peaks at 24 and returns to 0 . The two humps are two games — the well-posedness/stability marquee and the superposition-principle follow-oFigure 3: From the case study of Section 3 : named strategies present in the standing instruction file \mathcal{G} across its 36 revisions, by series (L/P/M/B). The staircase shape — flats punctuated by jumps at specific failures — is the signature of strategies earned rather than designed. The total grows 4\to 34 ; the four-series taxonomy crystallizes in one revision, and the process (P) series
