Vlasov-Maxwell-Landau平衡态的半自主形式化

Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium

March 16, 2026

作者: Vasily Ilin

cs.AI

摘要

我们完成了Vlasov-Maxwell-Landau（VML）系统中平衡态特征的完整Lean 4形式化，该系统描述了带电等离子体的运动。该项目展示了全流程AI辅助数学研究闭环：AI推理模型（Gemini DeepThink）根据猜想生成证明，智能编码工具（Claude Code）通过自然语言提示将其转化为Lean代码，专用证明器（Aristotle）完成了111条引理的闭合，最终由Lean内核验证结果。整个流程仅由一名数学家在10天内监督完成，成本200美元，且未编写任何代码。 项目开发过程完全公开：所有229条人类提示与213次git提交均存档于代码库。我们详细记录了AI的失效模式（假设蔓延、定义对齐错误、智能体规避行为）与成功经验（抽象/具体证明分离、对抗性自审、关键定义与定理陈述的人工审核）。值得注意的是，该形式化工作先于对应数学论文终稿的完成。

English

We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the full AI-assisted mathematical research loop: an AI reasoning model (Gemini DeepThink) generated the proof from a conjecture, an agentic coding tool (Claude Code) translated it into Lean from natural-language prompts, a specialized prover (Aristotle) closed 111 lemmas, and the Lean kernel verified the result. A single mathematician supervised the process over 10 days at a cost of \$200, writing zero lines of code. The entire development process is public: all 229 human prompts, and 213 git commits are archived in the repository. We report detailed lessons on AI failure modes -- hypothesis creep, definition-alignment bugs, agent avoidance behaviors -- and on what worked: the abstract/concrete proof split, adversarial self-review, and the critical role of human review of key definitions and theorem statements. Notably, the formalization was completed before the final draft of the corresponding math paper was finished.