🤖 AI

A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game

This paper presents a case study where a mathematician directs an AI system to formalize the mean-field derivation of the Vlasov equation in Lean 4, framing the process as a "strategy game" that successfully produced a complete, axiom-clean proof and a reusable optimal-transport library within approximately one month.

Original authors: Joseph K. Miller

Published 2026-07-13

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Joseph K. Miller

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a massive, high-stakes video game where the goal isn't to defeat a dragon, but to translate a complex, handwritten math proof into a language a computer can understand perfectly. This is the "Formalization Game" described in the paper. The players are a human mathematician and an AI assistant. The human acts as the Game Master, while the AI is the Builder.

The objective is simple: turn a paper written in LaTeX (a typesetting system for math) into code written in Lean 4 (a proof assistant). But there are strict rules to win. You don't just win by getting the code to run; you win only if the computer checks every single step and confirms the proof relies only on the most basic, unshakeable rules of logic, with no hidden shortcuts or "I'll fix this later" notes (called sorry) left behind.

The Three-Act Strategy

The paper breaks this game down into three distinct phases, like levels in a strategy game:

The Early Game (Setting the Rules): This is where the human Game Master does the heavy lifting. They must define exactly what the math objects are. If they define a "circle" slightly wrong, the whole game crashes later. The paper notes that in one instance, the team almost lost because they used a definition that accidentally made a test class empty (like trying to find a square circle). A human had to read the code and catch the error before the AI could waste time trying to prove things about nothing.
The Mid-Game (Breaking it Down): Here, the AI gets to work. The human breaks a giant, impossible theorem into smaller, bite-sized puzzles. The AI solves these smaller pieces. The paper emphasizes that the AI is great at the work, but the human is essential for the judgment—deciding which path to take and when to abandon a route that looks promising but is actually a dead end.
The End Game (The Cleanup): Eventually, the AI hits a wall where the math library doesn't have the tools it needs. The human has to decide: do we build a new tool from scratch, or is this a "phantom" gap that doesn't actually matter? The team successfully built a new tool (a bridge between two ways of measuring distance) and discarded the ones they didn't need.

The Big Win: The "Self-Contained Layer"

The most exciting part of the paper is what was left behind after the game was won. The team didn't just solve the specific problem of the Vlasov equation (which describes how particles move in a plasma or gas). They accidentally built a self-contained layer of general math tools.

Think of it like this: The team went to the forest to find a specific rare mushroom (the Vlasov equation solution). In the process, they built a brand-new, high-quality shovel and a map of the forest floor. The paper shows that this shovel and map are so well-made that anyone else can pick them up and use them for their own forest adventures, without needing the original mushroom.

The Numbers: The team created 299 total declarations (definitions and theorems). Of those, 49 formed this reusable "shovel and map" layer. This layer sits behind a small interface of 22 declarations.
The Time: The main "marquee" results took about one week, and the entire project took about one month.
The Cost: The team used a subscription service costing $200 per month (no extra charges per token).

What the Paper Says (and Doesn't Say)

The paper is very careful about what it claims. It explicitly rules out the idea that the AI can do this entirely on its own. The AI cannot decide what to prove or how to split the problems; it needs a human director. If the human steps back, the AI might hallucinate a proof or get stuck on a fake problem.

The paper also does not claim that this method solves the hardest, most mysterious problems in physics (like gravity with singular forces). It specifically chose a "smooth" version of the problem because that's where reusable tools can be built. The authors admit that for the really hard, messy problems, the missing ingredient is new math, not just better proof-checking.

The Takeaway

The paper suggests that the future of math isn't about replacing humans with robots. Instead, it's a partnership where the human is the strategic director and the AI is the execution engine. The human provides the taste, the judgment, and the vision; the AI provides the speed and the ability to check millions of tiny steps.

The authors are confident that this "game" framework works because they actually played it, won, and showed the replay. They aren't just suggesting it might work; they have the code, the logs, and the "self-contained layer" to prove it. However, they warn that the specific tools they used (the AI models) might change or disappear by the time you read this, but the strategy of how humans and machines should work together is what will last.

Technical Summary: A Formalization of the Mean-Field Derivation of the Vlasov Equation

Problem Statement
The paper addresses the challenge of formalizing complex, research-level mathematical results in the Lean 4 proof assistant. Historically, formalization has lagged behind mathematical discovery due to the labor-intensive nature of translating informal arguments into machine-checkable code, matching library conventions, and filling gaps in existing libraries (Mathlib). While recent AI systems can generate Lean proofs rapidly, two critical questions remain: (1) Can one trust proofs generated by an agent one did not write? and (2) Does the resulting code yield reusable mathematics, or is it disposable "glue" specific to a single problem?

Methodology: The Formalization Game
The authors frame the formalization process as a "game" with precise rules, separating the roles of a human mathematician (the director) and an AI agent (the executor). The methodology is structured into three phases:

Early Game (Definitional Scoping): The human mathematician translates the target theorems and their underlying definitions into Lean, leaving proofs as sorry. The goal is to "lock" the API (signatures and definitions) before proving anything. This prevents errors in definitions (e.g., incorrect regularity classes or metric spaces) from propagating through the entire development.
Mid Game (Steering Decomposition): The human directs the AI to decompose large, unprovable theorems into smaller, tractable sub-lemmas. The AI executes the proofs of these sub-lemmas. The human's critical role is "steering": deciding where to cut a theorem, which mathematical route the library can support, and when to abandon a failing strategy.
End Game (Triage of Library Gaps): The remaining sorrys are triaged. They are classified as:
- Phantoms: Apparent gaps that dissolve upon closer reading of the requirements.
- Genuine Gaps to Build: Standard mathematics missing from the library that the team formalizes from primitives.
- Genuine Gaps to Defer: True mathematical gaps marked with explicit placeholders (cited theorems) rather than built, if they are not essential to the core result.

Win Conditions and Reusability
The paper introduces two machine-checkable criteria to validate the work:

The Win Condition: The development compiles with no sorrys, and the command #print axioms confirms that the target theorems depend only on Lean's foundational axioms (propext, Classical.choice, Quot.sound). This certifies the proof's soundness relative to the written statement.
The Self-Contained Layer: A subset of the development is extracted that contains general mathematics reusable by the wider library. This layer must pass four checks:
1. Isolation: No dependencies run from the general layer to the problem-specific code (reverse-edge count is 0).
2. Standalone Compilation: The layer compiles against Mathlib alone, with no problem-specific imports.
3. Linter-Clean: The code passes the library's automated linter suite with zero warnings.
4. Non-redundant: No declarations restate existing library results.

Key Contributions and Results
The case study formalizes Dobrushin's derivation of the nonlinear Vlasov equation from $N$ -particle Hamiltonian dynamics. The formalization covers:

Well-posedness: Existence and uniqueness of solutions for the nonlinear Vlasov equation.
Stability: Dobrushin's stability estimate in the Wasserstein-1 metric ( $W_1$ ).
Mean-Field Limit: The convergence of the empirical measure of $N$ particles to the Vlasov solution.
Superposition Principle: A short-window result showing that weak solutions are Lagrangian (transported by characteristic flows), requiring an additional regularity assumption ( $C^2$ potential).

Specific Technical Outcomes:

Optimal Transport Machinery: The build generated a self-contained layer of optimal transport mathematics (49 declarations, 22-declaration interface) including the $W_1$ metric in both primal (coupling) and dual (Kantorovich–Rubinstein) forms, and the duality bridge between them. This layer compiles against Mathlib alone.
Human-AI Division of Labor: The human mathematician did not write proofs but directed the strategy. Key human interventions included:
- Correcting a "silent collapse" in the weak-solution test class (where a definition of $C^\infty$ was actually $C^\omega$ , making the test class empty).
- Steering the proof of the Kantorovich–Rubinstein duality by rejecting Hilbert-space approaches and guiding the agent to use Farkas' lemma and geometric separation.
- Redirecting the stability proof from a dual formulation (requiring an unproven attainment theorem) back to Dobrushin's original coupling formulation, which the library could support.
- Deciding that the superposition principle requires $C^2$ regularity (AssW2) to ensure the characteristic flow is $C^1$ , a nuance extracted from the prose and encoded into a typeclass.
Timeline and Cost: The well-posedness and stability results were completed in about one week; the full development (including the superposition principle) took about one month. The cost was approximately $200 (a flat-rate subscription), with no manual Lean coding by the human.

Significance and Claims
The paper claims that this "strategic director" model allows formalization to keep pace with ordinary mathematical work.

Trust: Trust is established not by the human reading every line of the proof, but by the machine-checkable win condition (axiom footprint) and the human's oversight of the definitions and decomposition strategy.
Reusability: The work demonstrates that AI-assisted formalization can yield "absorbable" mathematics (the self-contained layer) rather than disposable code.
Methodological Longevity: The "game" framing is designed to outlast specific AI tools. The rules (win conditions, phases, strategy framework) are tool-agnostic. The paper argues that while the specific AI agents and libraries will evolve, the division of labor—where the human provides mathematical judgment and the machine provides execution—remains a viable and scalable strategy.
Limitations: The authors are modest, noting that the "self-contained layer" check was applied to a single project and that the extracted layer still imports Mathlib wholesale rather than minimally. The timeframe is a single observation dependent on the human director's fluency. The paper does not claim to solve the "singular" force case (e.g., gravity) but focuses on the smooth case where reusable libraries can be built.

The paper concludes that the "craft" of formalization is shifting from writing proofs to directing agents, managing the "repertoire of moves" (heuristics, decomposition strategies, and library triage) that allow complex analysis to be certified.

The Three-Act Strategy

The Big Win: The "Self-Contained Layer"

What the Paper Says (and Doesn't Say)

The Takeaway

Technical Summary: A Formalization of the Mean-Field Derivation of the Vlasov Equation

More like this