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

Vlasov 方程平均场推导的形式化：作为策略游戏的 AI 辅助 Lean 形式化

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.

我们通过让数学家指导 AI 系统，在 Lean 4 证明助手（proof assistant）中对一项研究成果进行了形式化，并将这一过程构建为一场“形式化游戏”。游戏的目标是将 LaTeX 文档转化为 Lean 代码。当开发项目能够成功编译、不包含任何“sorry”（未完成证明的占位符），且机器检查确认目标定理仅建立在 Lean 的基础公理之上时，即视为游戏获胜。

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).

“复用性”是第二项检查标准，根据我们引入的定义：该开发成果是否产生了一个可被更广泛的库所吸收的、自包含的通用数学层。本案例研究是对非线性 Vlasov 方程适定性（well-posedness）的完整、公理化形式化，采用了 Dobrushin 的平均场路径——包括存在性、唯一性、稳定性估计和平均场极限，以及短时间窗口叠加原理（弱解是拉格朗日解）。

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.

人类的角色是指导而非编写证明：负责界定定义范围、引导分解过程并梳理库中的缺失部分；而 AI 代理则负责执行。形式化过程证明了所写出的每一条陈述的正确性；至于所写的陈述是否为预期的定理，则仍由数学家进行判断。

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.

构建过程中产生的最优传输机制（特别是 Wasserstein-1 度量的性质和 Kantorovich-Rubinstein 对偶定理）被分离为一个自包含层，仅需 Mathlib 即可编译：这部分约占整个开发工作的六分之一（299 个声明中的 49 个），并通过一个包含 22 个声明且无反向依赖的接口进行封装。核心定理的实现耗时约一周，完整开发耗时约一个月。

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.

我们报告的定量结论仅作为单次游戏的观察结果，而非通用法则。游戏规则并未指定任何特定系统，因此这种方法论框架旨在超越单次运行所使用的具体工具。