我们在Lean 4证明助手中形式化了一项研究结果，过程由数学家指导AI系统，并将这一活动框架化为一个形式化游戏。目标是将LaTeX文档转化为Lean代码。游戏获胜的标准是开发成功编译，无错误，并且机器检查显示目标定理仅依赖于Lean的基础公理。我们引入的第二个检查是重用性：即开发是否生成一个自包含的数学层，能够被更广泛的库吸收。
本案例研究是通过Dobrushin的均场路径对非线性Vlasov方程的良定性进行完整的公理清晰形式化——包括存在性、唯一性、稳定性估计和均场极限，以及短时间窗口的叠加原理（弱解为拉格朗日形式）。在此过程中，人的角色是指导，而非撰写证明：负责定义的范围、指导分解，以及处理库中的空白；AI代理则执行具体任务。形式化过程为每个陈述的证明提供了认证；而书面陈述是否为意图定理则仍由数学家判断。
从构建中产生的最优传输工具（特别是Wasserstein-1度量和Kantorovich-Rubinstein对偶定理的性质）分离出一个自包含的层，与Mathlib独立编译：约占开发的六分之一（299个声明中的49个），并通过一个没有反向依赖的22声明接口连接。主要定理在约一周内运行，完整开发则在一个月内完成。我们报告的定量声明是一次游戏的观察，而非普遍法则。游戏规则未指定特定系统，因此方法论框架旨在超越任何一次运行的工具。