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

技术摘要：Vlasov 方程平均场推导的形式化研究

问题陈述
本文旨在解决在 Lean 4 证明助手中实现复杂、研究级数学结果的形式化这一挑战。从历史上看，由于将非形式化论证转化为机器可检查代码的过程需要大量的人力投入（包括匹配库约定以及填补现有库 [Mathlib] 中的空白），形式化进程一直滞后于数学发现。虽然近期的 AI 系统可以快速生成 Lean 证明，但仍有两个关键问题存在：(1) 人能否信任一个并非由自己编写的智能体所生成的证明？(2) 生成的代码是产生可复用的数学成果，还是仅针对特定问题的、一次性的“胶水”代码？

方法论：形式化游戏
作者将形式化过程框架化为一个具有精确规则的“游戏”，并将人类数学家（导演）与 AI 智能体（执行者）的角色分离。该方法论分为三个阶段：

1. 前期游戏（定义范围界定）： 人类数学家将目标定理及其底层定义翻译为 Lean，并将证明部分留为 sorry。其目标是在进行任何证明之前“锁定” API（签名与定义）。这可以防止定义错误（例如：错误的正则类或度量空间）在整个开发过程中传播。
2. 中期游戏（转向分解）： 人类指导 AI 将大型且不可证明的定理分解为较小的、可处理的子引理。AI 执行这些子引理的证明。人类的关键作用是“转向”（steering）：决定在哪里切割定理、选择库可以支持的数学路径，以及何时放弃失败的策略。
3. 后期游戏（库缺口分类）： 对剩余的 sorry 进行分类处理。它们被分为：
   • 幻影（Phantoms）： 仔细阅读要求后便会消失的表象缺口。
   • 真实的构建缺口（Genuine Gaps to Build）： 库中缺失的标准数学知识，由团队从原语开始构建。
   • 真实的延迟缺口（Genuine Gaps to Defer）： 真正的数学缺口，通过显式占位符（引用的定理）而非直接构建来标记，若其对核心结果并非必不可少，则予以搁置。

获胜条件与可复用性
论文引入了两个可机器检查的标准来验证工作成果：

• 获胜条件： 开发过程编译通过且无 sorry，并且 #print axioms 命令确认目标定理仅依赖于 Lean 的基础公理（propext, Classical.choice, Quot.sound）。这证明了证明相对于所写陈述的正确性。
• 自包含层： 从开发中提取出一个包含可供更广泛库使用的通用数学内容的子集。该层必须通过四项检查：
  1. 隔离性： 通用层到特定问题代码的依赖关系为零（反向边计数为 0）。
  2. 独立编译： 该层仅针对 Mathlib 进行编译，不依赖特定问题的导入。
  3. 无 Linter 警告： 代码通过库的自动化 linter 套件且零警告。
  4. 非冗余性： 没有声明重复现有的库结果。

主要贡献与结果
案例研究形式化了 Dobrushin 关于从 $N$ 粒子哈密顿动力学导出非线性 Vlasov 方程的推导过程。形式化涵盖了：

• 适定性（Well-posedness）： 非线性 Vlasov 方程解的存在性与唯一性。
• 稳定性（Stability）： 在 Wasserstein-1 度量（$W_1$）下的 Dobrushin 稳定性估计。
• 平均场极限（Mean-Field Limit）： $N$ 粒子经验测度向 Vlasov 解的收敛性。
• 叠加原理（Superposition Principle）： 一个短窗口结果，表明弱解是拉格朗日型的（由特征流传输），这需要额外的正则性假设（$C^2$ 势函数）。

具体技术成果：

• 最优传输机制： 构建生成的层包含了一个自包含的最优传输数学层（49 个声明，22 个声明的接口），包括原始形式（耦合）和对偶形式（Kantorovich–Rubinstein）下的 $W_1$ 度量，以及两者之间的对偶桥梁。该层可独立于问题代码编译。
• 人机分工： 人类数学家并未编写证明，而是指导策略。关键的人类干预包括：
  • 纠正了弱解测试类中的“隐性崩溃”（即原本应为 $C^\infty$ 的定义实际上是 $C^\omega$，导致测试类为空）。
  • 引导 Kantorovich–Rubinstein 对偶性的证明，拒绝了希尔伯特空间方法，并指导智能体使用 Farkas 引理和几何分离。
  • 将稳定性证明从对偶形式（需要未证明的达到定理）转向回 Dobrushin 最初的耦合形式，因为库可以支持后者。
  • 判定叠加原理需要 $C^2$ 正则性（AssW2）以确保特征流是 $C^1$ 的，这一细微差别从文本中提取并编码进了类型类（typeclass）中。
• 时间线与成本： 适定性和稳定性结果在大约一周内完成；完整开发（包括叠加原理）耗时约一个月。成本约为 200 美元（固定订阅费），且人类无需手动编写 Lean 代码。

意义与主张
论文声称，这种“战略导演”模型使形式化能够跟上普通数学工作的步伐。

• 信任： 信任并非建立在人类阅读每一行证明的基础上，而是建立在机器可检查的获胜条件（公理足迹）以及人类对定义和分解策略的监督之上。
• 可复用性： 本工作证明了 AI 辅助的形式化可以产生“可吸收”的数学（自包含层），而非一次性的代码。
• 方法论的长效性： “游戏”框架的设计旨在超越特定的 AI 工具。其规则（获胜条件、阶段、策略框架）是工具无关的。论文认为，尽管具体的 AI 智能体和库会不断演进，但这种分工——即人类提供数学判断，机器提供执行——是一种可行且可扩展的策略。
• 局限性： 作者保持了谦逊，指出“自包含层”的检查仅应用于单个项目，且提取层仍大规模导入 Mathlib 而非极简导入。时间线是基于人类导演流畅度的单一观察。论文并不声称解决了“奇异”力（如引力）的情况，而是专注于可以使用可复用库的平滑情况。

论文总结道，形式化的“手艺”正在从编写证明转向指导智能体，管理那些允许复杂分析得到认证的“招式谱系”（启发式、分解策略和库分类）。