Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Vasily Ilin

Abstract

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.

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

Abstract

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.
Paper Structure (41 sections, 1 theorem, 1 equation, 12 figures, 3 tables)

This paper contains 41 sections, 1 theorem, 1 equation, 12 figures, 3 tables.

Table of Contents

  1. Introduction
  2. The Theorem
  3. The Physical System
  4. Main Result
  5. Proof Architecture
  6. Tools
  7. Claude Code
  8. Gemini DeepThink
  9. Aristotle
  10. Lean LSP tools.
  11. Process
  12. Timeline
  13. Phase 1: Natural-Language Proof (Feb 28)
  14. Phase 2: Scaffolding (Mar 1 -- 2)
  15. Phase 3: Abstract Proof Chain (Mar 3 -- 7)
  16. ...and 26 more sections

Key Result

Theorem 1

Let $f > 0$ be a smooth steady-state solution of the VML system with Coulomb collisions on $\mathbb{T}^3 = (\mathbb{R}/\mathbb{Z})^3$, with Schwartz-class velocity decay and a polynomial log-growth bound. Then:

Figures (12)

  • Figure 1: ArXiv papers using Lean for formalization, by year. Data from the arXiv metadata snapshot (March 2026), filtered for references to the Lean theorem prover.
  • Figure 2: The formal Lean 4 statement of the main theorem (CoulombConcreteTheorem42). The proof (omitted) is 80 lines of tactic invocations that assemble the seven-step argument described in \ref{['sec:proof-arch']}. Here Torus3 is Fin 3 $\to$ AddCircle 1, periodicLift lifts torus functions to $\mathbb{R}^3$ for differentiation, and equilibriumMaxwellian is the Maxwellian $\rho_{\mathrm{ion}}/(2\pi T)^{3/2}\exp(-|v|^2/2T)$.
  • Figure 3: Proof dependency graph, generated with LeanBlueprint leanblueprint. All nodes are green (fully proved). The graph flows from primitive definitions (normSq, eucNorm, landauMatrix) at the top through intermediate results (H_theorem, D_zero_implies_maxwellian, the field and conservation lemmas) down to theorem42 and its concrete Coulomb instantiation coulomb_concrete at the bottom. An interactive version is available in the repository.
  • Figure 4: Sorry count in main/ over time (85 commits). The sawtooth pattern reflects alternating phases of scaffolding (sorry's accumulate) and proving campaigns (sorry's eliminated). Key events: peak 25 on Mar 2 (abstract proof chain stated); Aristotle drops count from 25$\to$7 on Mar 3; first 0 sorry's on Mar 7 (abstract theorem proved); $+$35 sorry's on Mar 8 (Coulomb kernel instantiation begun); 35$\to$0 sprint on Mar 9; brief $+$1 on Mar 10 (non-vacuousness theorem, immediately resolved).
  • Figure 5: Lean lines of code over time (all 213 commits). The project progressed in four phases: (1) Abstract proof chain (Mar 3 -- 6), formalized against an abstract FlatTorus3 typeclass. (2) Coulomb kernel analysis (Mar 7 -- 9), handling the singularity at $r=0$ -- the sharp LOC increase reflects $\sim$4K lines of analytical estimates. (3) Cleanup (Mar 10, early): $\sim$3K lines of dead code, redundant lemmas, and unnecessary heartbeat overrides removed. (4) Non-vacuousness (Mar 10, late): satisfiability of the 12 hypotheses.
  • ...and 7 more figures

Theorems & Definitions (1)

  • Theorem 1: Informal