← 返回 2026-03-18

Vlasov-Maxwell-Landau 平衡态的半自主形式化 Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium

Vasily Ilin 📅 2026-03-16 👍 15 2026-07-13 08:36

AI 辅助数学 Lean 4 形式化验证数学物理自动定理证明

arXiv HuggingFace PDF

首个完整的 AI 辅助数学研究闭环演示，从猜想到 Lean 4 形式化验证仅需 10 天

前置知识

形式化验证

使用数学证明助手（如 Lean 4）将数学定理和证明转换为计算机可以检查的严格形式语言。每个推理步骤都必须通过内核验证，确保逻辑正确性。相比传统数学证明，形式化验证消除了人类的直觉跳跃和潜在错误，但要求极高的精确性。

本文展示如何让 AI 自动完成这一传统上需要数月学习 Lean 4 和大量编码的任务

Vlasov-Maxwell-Landau 系统

描述带电等离子体动力学的偏微分方程组，包含粒子分布函数 f(t,x,v)、电场 E(t,x) 和磁场 B(t,x)。Vlasov 方程描述粒子在电磁场中的运动，Maxwell 方程描述电磁场的演化，Landau 碰撞算子处理带电粒子间的库仑碰撞。这是一个耦合的非线性系统，分析难度极高。

本文形式化的是该系统的稳态平衡态表征定理，是数学物理中的硬分析问题

定理证明助手

基于类型论的交互式证明系统，如 Lean 4、Coq、Isabelle。它们提供形式化数学语言（如 Lean 的依赖类型论）和自动化工具（策略引擎）。Lean 4 的内核会验证每个证明步骤，确保没有逻辑漏洞。'sorry' 是 Lean 中标记未完成证明的占位符。

本文使用 Lean 4 作为最终的验证工具，111 个引理由 Aristotle 自动证明，186 个引理最终全部消除 sorry

假设原则

形式化中的核心原则：遇到困难的引理时，应该用 sorry 标记为待证引理，而不是将其作为主定理的假设。添加假设会削弱定理的适用范围，而 sorry 只是标记证明缺口。这是 AI 形式化中最容易违反的原则，因为 AI 倾向于选择能立即编译通过的路径。

本文发现 Claude Code 的主要失败模式就是假设蔓延，从 42 个假设精简到 12 个物理有意义的假设

研究动机

传统数学形式化需要同时精通数学和证明助手，学习曲线陡峭。即使经验丰富的数学家也需要数月才能形式化只需几页纸证明的结果。这限制了形式化验证的应用范围。现有 AI 辅助形式化工作主要集中在竞赛数学或教科书结果，针对研究级分析问题的完整形式化仍是空白。2026 年的现有项目中，Gauss 使用专家编写的 22K 行定义，仅消除 160K sorry；Numina 需要 13 名专家协作；AxiomProver 虽然完全自主，但形式化的结果都是简短的组合或代数论证，而非需要硬分析的大规模形式化。

本文的目标是本文的目标是演示完整的 AI 辅助数学研究闭环：从开放猜想出发，通过 AI 推理模型生成无需修正的自然语言证明，再由 AI 编码代理将证明转化为 Lean 4 代码，云自动定理证明器证明引理并捕获错误猜想，最终由 Lean 内核提供逻辑正确性保证。整个过程由单一数学家监督，10 天完成，零行人工编写代码。同时形式化数学物理中的新定理——完整 VML 系统稳态平衡态的完整表征，包括库仑碰撞和电磁耦合。

与已有工作不同的是，本文的独特切入角度在于结合了多个此前项目所未有地同时具备的特征：规模和深度（34 文件、10K+ 行 Lean 代码，涉及硬分析中的库仑奇点消去、莱布尼茨积分规则、环面能量方法）、新理论（定理甚至无法用现有 Mathlib 陈述——Landau 算子、环面微分结构、VML 系统必须从零定义）、新结果（完整 VML 系统光滑稳态的精确表征在文献中未以此形式出现）、完全透明的过程（单一数学家零代码写作，每个提示、提交、工具调用都公开）。与 AxiomProver 的完全自主相比，本文虽然不是完全自主，但展示了更复杂数学研究的可行工作流程。

核心方法

本文采用四阶段 AI 协同工作流程。直觉上，数学家的角色从证明执行者变为监督者，提出猜想并评估定理陈述的正确性。技术路线上，首先由 Gemini DeepThink 生成自然语言证明蓝图，然后 Claude Code 将其翻译为 Lean 4 代码，期间通过 Aristotle 云证明器自动化证明引理并捕获错误猜想，最后 Lean 内核验证最终结果。关键设计原则包括：假设原则（用 sorry 标记缺口而非添加假设）、抽象/具体分离（先形式化抽象 FlatTorus3 接口，再实例化具体环面）、对抗性自评（/critique 命令模拟审稿人找弱点）。

核心创新点是将数学研究的完整闭环自动化，且每个阶段使用专用的 AI 系统：Gemini DeepThink 擅长数学推理，生成完整的自然语言证明；Claude Code 擅长代码生成，将证明转化为 Lean 4；Aristotle 擅长自动定理证明，关闭引理；Lean 内核提供最终正确性保证。与已有方法的本质区别在于：Gauss 使用专家编写的定义，仅消除 sorry；Numina 需要人类协作编写 Lean 代码；AxiomProver 完全自主但针对简短结果。本文使用四个 AI 系统，数学家仅负责提出猜想、检查定理陈述、执行假设原则、提供数学直觉、设计自动化套件。

方法步骤详情

方法分为六个阶段。第一阶段（2月28日）：数学家向 Gemini DeepThink 提出问题，Gemini 产生详细的六步证明，识别相关文献，五轮对话后无需数学修正。第二阶段（3月1-2日）：Claude Code 生成单文件 1000+ 行 Lean 代码，用 sorry 标记缺口，估计需数月完成。数学家强制执行假设原则：遇到困难引理时用 sorry 标记而非添加假设。第三阶段（3月3-7日）：单文件拆分为 main/ 目录，FlatTorus3 类型类抽象空间域，指定分部积分、旋度散度恒等式、最大值原理、调和函数常值性等 22 个字段。TorusInstance 模块证明环面满足所有字段。3月7日抽象定理达到 0 sorry。第四阶段（3月7-8日）：引入对抗性自评 /critique 和 /babysit 自动化循环（11 个步骤），执行 122 个文档化周期。第五阶段（3月8-9日）：库仑核实例化，证明 Landau 碰撞算子满足 VelocityDecayConditions bundle 的 17 个可积性、可微性、连续性条件。库仑奇点导致近似范数的负一次方行为，在三维欧氏空间中勉强可积。每个可积性证明需要分解域（原点附近的球用局部可积性，补集用 Schwartz 衰减），产生约 4000 行分析估计。3月9日 11:15 PM 库仑定理达到 0 sorry。第六阶段（3月10日）：清理阶段移除 3K 行死代码，非空性定理验证 12 个假设的可满足性。

技术新颖性

技术新颖性体现在多个方面。抽象/具体分离：FlatTorus3 类型类先形式化数学论证，再实例化具体环面，当环面证明需要重写时抽象证明链完全不受影响。对抗性自评：/critique 命令模拟 hostile reviewer，识别错误假设、不必要假设、死代码，部分自动化了人类监督。自动化循环：/babysit 在两台机器上并发执行，实现近乎全天候的开发。库仑奇点估计：将域分解为原点附近和补集，使用局部可积性和 Schwartz 衰减，是形式化分析的创新。假设原则系统化：将 15 个分散的速度空间衰减条件捆绑为单一 VelocityDecayConditions 结构，将正则性事实如密度的连续性在证明内部从支配界限推导。非空性定理：形式化平衡态 Maxwellian 满足所有 12 个假设，提供了健全性检查。

**Figure 3**: Proof dependency graph, generated with LeanBlueprint.

**Figure 6**: Claude Code activity across two machines (local + university server).

**Figure 8**: Tool usage across 17,334 invocations.

**Figure 11**: LOC by file group over time.

实验结果

核心发现包括：完整 Lean 4 形式化包含 34 个文件、10,445 行代码、39 个定理、186 个引理、28 个定义，0 个 sorry。开发周期 10 天，213 个 git 提交，32 个 Claude Code 会话（跨两台机器），229 个人类提示，122 个 /babysit 周期，27,186 个助手轮次，17,334 个工具调用。消耗 28 亿输入 token、1100 万输出 token，输入输出比 254:1，反映形式化验证的重读特性。Aristotle 提交 220 次，证明 111 个（50%）、反驳 28 个（13%）、返回 sorry 66 个（30%）、失败 15 个（7%）。反驳的陈述特别有价值，早期捕获错误猜想：缺失可测性假设、Vitali 集合反例、库仑核的错误 Schwartz 衰减估计。Aristotle 总体中位周转时间 19 分钟：证明引理中位 9 分钟，反驳陈述 29 分钟，返回 sorry 中位 5.6 小时。开发轨迹显示 sorry 计数的锯齿模式和 LOC 历史的四阶段结构（抽象证明链、库仑核分析、清理、非空性）。最终代码库约一半是支撑基础设施（定义、环面实例、库仑核可积性文件、衰减助手），反映 Mathlib 当前覆盖与研究级数学物理所需背景材料的巨大差距。

**Table 1**: Recent research-level formalizations with publicly available code, sorted by LOC.

**Table 2**: Project timeline and sorry count evolution.

**Figure 4**: Sorry count in main/ over time (85 commits).

**Figure 5**: Lean lines of code over time (all 213 commits).

**Figure 7**: Token consumption across the project.

**Figure 9**: Outcomes of 220 Aristotle submissions.

**Figure 10**: Aristotle turnaround times for 214 submissions, colored by outcome.

**Figure 12**: Lines of Lean code added and deleted per day.

查看结构化数据

任务	指标	本文	基线	提升
VML 平衡态定理形式化	Lean 代码行数	10,445 行	Gauss: 181K 行 (消除 160K sorry)，Numina: ~8K 行，AxiomProver: 4.3K/2.7K/0.2K 行	针对新理论和新结果，规模介于 Numina 和 Gauss 之间
自动定理证明	Aristotle 证明率	111/220 = 50%	无直接对比（首次报告完整 Aristotle 性能）	首次报告 Aristotle 在研究级形式化中的表现
开发周期	天数	10 天	传统形式化：数月到数年	大幅降低门槛，从数年 Lean 专业知识到监督 AI 代理
人力投入	人工代码行数	0 行	Gauss: 22K 行专家定义，Numina: 13 名专家协作，Bayer: 20K 行	首个数学家零代码的形式化项目
成本	美元	200 订阅	API 等价成本 ~6,300（缓存）或 ~42,700（无缓存）	Claude Max 计划的无限制使用模式大幅降低门槛

局限与改进

作者承认的局限性包括：数学新颖性——稳态为全局 Maxwellian 的定理在文献中未以此精确形式陈述和证明，但每个证明技术都是经典的（H 定理和 Landau 算子零空间表征是标准的，多项式匹配强制常数温度和 Killing 方程出现在相关文献，最大值原理是教科书）。新意在于完整静态表征的组装，特别是洛伦兹力仅贡献 O(|v|^1) 项的观察（因为向量叉乘与自身点积为零），使得 O(|v|^3) 和 O(|v|^2) 约束不变；安培定律积分论证强制整体速度为零；高斯定律与中性背景的闭合。定义对齐——Mathlib 维护者立即识别出定义对齐 bug：原定理使用 ContDiff R top，在 Mathlib 中意味着解析而非预期的无穷阶可微，修复后定理更强（假设更少）。这说明了 AI 生成形式化的根本风险：代码编译且证明检查，但定理不陈述预期的内容。复现性——过程依赖特定模型版本的特定能力，这些模型频繁更新。成本——虽然订阅成本是 200 美元，但 API 等价成本是约 6,300 美元（缓存）或约 42,700 美元（无缓存），差距反映 Claude Max 计划的无限制使用模型。无缓存定价下项目不会如此可及。人力——虽然未编写代码，但过程需要大量数学专长和约 50 小时主动监督。需要数学家足够理解证明以检测代理何时削弱定理。

独立分析的弱点

独立分析的弱点包括：定义对齐风险——原定理使用 ContDiff R top（解析）而非预期的无穷阶可微，Mathlib 维护者立即识别但 AI 和数学家在 10 天开发中未发现。改进方向：引入定义验证模块，在形式化前自动检查关键定义与意图的语义对齐；使用 AI 专门进行定义审查，建立定义意图的形式化注释系统。假设蔓延虽然被控制，但仍需人工强制执行。改进方向：开发假设审计工具，自动检测假设是否应该是可推导引理；在项目文档中编码更强的假设原则约束。自动化在处理新颖证明策略时效果不佳——代理经常陷入循环，重试相同失败方法而非重新考虑证明策略。改进方向：引入策略记忆和模式识别，当某个策略失败多次时自动建议替代方案；开发证明规划器，在形式化前生成高层证明策略树。架构决策需要人类判断——选择表示、结构化类型类、决定抽象什么需要人类判断。改进方向：建立表示选择的形式化标准库；开发自动抽象建议系统，根据定理特征推荐适当的抽象层次。库仑奇点估计产生约 4000 行分析估计，代码量巨大。改进方向：开发分析估计的自动化模式，将奇点分解方法封装为可复用模板；使用专用分析工具自动生成本地可积性和衰减估计。

未来方向

作者提出的未来方向包括：将本文的工作流程——猜想、生成证明、形式化、验证、审查——作为计算机辅助数学研究的常见模式。每个阶段现在都在当前 AI 系统能力范围内：推理模型可以解决猜想并产生详细证明，编码代理可以将这些证明转化为形式语言，自动证明器可以关闭缺口并捕获错误，证明内核提供正确性的最终保证。基于成果可延伸的方向包括：扩展到更复杂的数学物理系统（Landau 碰撞的动力学稳定性、VML 系统的时间依赖分析、其他等离子体模型）；形式化更多分析估计技术（奇点消去、能量方法、调和分析）；开发更多专用自动定理证明器（针对 PDE、分析、几何）；建立形式化数学的版本控制和协作平台；探索 AI 生成的定理和猜想。特别有前景的是将非空性定理系统化——为每个形式化定理自动生成验证假设可满足性的定理，作为健全性检查。另一个方向是发展专家级 AI 定义审查——使用专门训练的模型检测定义与意图的语义对齐问题，减少对人类专家的依赖。

复现评估

复现评估：项目完全开源，所有 229 个人类提示（带时间戳）、213 个 git 提交、完整 Gemini 对话、所有 122 个 /babysit 周期的完整开发日志都公开。仓库地址在 GitHub。数据：不需要额外数据集，形式化的是纯数学定理。算力：本文在两台机器上运行（本地 + 大学服务器），支持并发 /babysit 循环。核心工具：Claude Code（200 美元/月订阅）、Gemini DeepThink（免费或低成本）、Aristotle（项目期间免费）、Lean 4（开源）。难度：中等。不需要 Lean 4 专业知识，但需要足够的数学专长以理解证明并检测假设削弱。主要挑战在于理解 Mathlib 的标准库和类型论基础，虽然 AI 可以生成大部分代码，人类仍需阅读关键定义和定理陈述以验证对齐。成本：API 等价成本约 6,300 美元（缓存）或约 42,700 美元（无缓存），但 Claude Max 订阅仅 200 美元，大幅降低门槛。主要依赖是特定模型版本，模型更新可能影响复现。

论文图表

**Figure 1**: ArXiv papers using Lean for formalization, by year.
该图展示了使用 Lean 进行形式化的 arXiv 论文数量随年份的增长趋势。从 2020 年开始缓慢增长，2023-2024 年加速，2025 年和 2026 年初显著增加，反映了 AI 辅助形式化工具的成熟。数据来自 2026 年3月的 arXiv 元数据快照，筛选引用 Lean 定理证明器的论文。

这张图说明了 AI 辅助形式化的快速发展趋势，为本文的工作提供了背景。它展示了 Lean 在研究界应用的加速增长，解释了为什么 2026 年是进行本文工作的时机。图中的趋势也暗示了 AI 工具（如 Claude Code、Aristotle）在降低形式化门槛方面的成功。

Figure 2: The formal Lean 4 statement of the main theorem (CoulombConcreteTheorem42).

该图展示了主定理的形式化 Lean 4 陈述。定理有 12 个假设：碰撞频率大于零、离子密度大于零、分布函数正性、分布函数在速度上三阶连续可微、在空间上二阶连续可微（周期提升）、磁场在空间上二阶连续可微、Schwartz 类衰减、多项式对数增长界、Vlasov 方程、安培定律、高斯定律、磁场散度为零。结论：存在平衡温度和常值磁场使得分布函数为平衡态 Maxwellian，电场为零，磁场为常值。

这张图展示了本文形式化工作的核心成果——完整的 Lean 4 定理陈述。12 个假设每个都有明确的物理意义，反映了假设原则的成功（从 42 个假设精简到 12 个）。定理陈述的精确性也展示了形式化验证的价值——每个条件都明确编码，无歧义。这是理解本文技术贡献的关键。