发表机构
Stanford University; Massachusetts Institute of Technology（斯坦福大学; 麻省理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究以数学家指导AI在Lean 4中形式化研究成果为案例，将其构建为形式化游戏。通过此方式对非线性弗拉索夫方程适定性完整形式化，展示了开发过程及成果，还介绍了最优传输机制的分离情况及开发时间等，为形式化研究提供了新方法。
AI 中文摘要
我们通过让数学家指导人工智能系统，在Lean 4证明助手里将一项研究成果形式化，并将此活动构建为一个形式化游戏。目标是把一个LaTeX文档转化为Lean。当开发代码能编译、无“抱歉”语句且机器检查表明目标定理仅基于Lean的基础公理时游戏获胜。重用是第二项检查，通过我们引入的定义判断：开发成果能否产生一个更广泛库可吸收的自包含通用数学层。案例研究是通过多布鲁申平均场路径对非线性弗拉索夫方程适定性进行完整、无公理的形式化，包括存在性、唯一性、稳定性估计和平均场极限，以及短窗口叠加原理（弱解是拉格朗日的）。人类负责指导而非编写证明，人工智能执行。形式化证明了每个书面陈述；书面陈述是否为预期定理仍由数学家判断。构建过程中出现的最优传输机制（特别是瓦瑟斯坦-1度量的性质和康托罗维奇-鲁宾斯坦对偶定理）分离成一个仅针对Mathlib编译的自包含层：约占开发内容六分之一（299个声明中的49个），位于一个无反向依赖的22个声明接口之后。主要定理运行约一周，完整开发约一个月。我们将定量结果作为一场游戏的观察报告，而非普遍规律。游戏规则未指定特定系统，所以方法框架旨在比任何一次运行的工具更持久。
英文摘要
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. 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). 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. 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. 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.
Comments26 pages, 4 figures. Lean 4 development, blueprint site, and agent logs: https://github.com/Hydrodynamical/Vlasov_Meanfield_Formalization
