AI辅助数学证明：将Vlasov方程推导过程转化为“形式化游戏”

近日，一项发表于arXiv的研究展示了一种创新的数学证明形式化方法。研究团队将Vlasov方程的平均场推导过程转化为Lean证明助手可验证的形式化证明，并将整个过程设计成一种“形式化游戏”。

在这种游戏化框架中，数学家的角色是指挥者而非证明书写者：负责定义范围、指导分解过程、识别数学库的缺失部分；而AI代理则负责执行具体的证明任务。游戏的目标是将LaTeX文档转化为Lean代码，获胜条件是开发项目能够编译通过、不含未完成证明（sorry），且机器检查确认目标定理仅依赖于Lean的基础公理。

案例研究完整形式化了非线性Vlasov方程通过Dobrushin平均场路径的适定性问题，包括存在性、唯一性、稳定性估计和平均场极限，以及短时叠加原理。整个开发过程产生了约300个声明，其中最优传输工具（特别是Wasserstein-1度量和Kantorovich-Rubinstein对偶定理的性质）形成了一个独立层，约占开发的六分之一。

研究团队强调，该方法论框架不依赖于特定系统，旨在超越单次运行所使用的工具。主要定理的证明耗时约一周，完整开发约一个月完成。这项研究展示了人机协作在数学形式化领域的潜力，为复杂数学证明的验证提供了新思路。