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

TL;DR

This paper details a fully formalized proof of the Vlasov-Maxwell-Landau equilibrium using Lean 4, showcasing AI-assisted research with minimal human coding over 10 days.

Contribution

It demonstrates a complete AI-assisted formalization process for a complex plasma physics system, including lessons on AI failure modes and effective strategies.

Findings

AI reasoning and coding tools can collaboratively formalize complex mathematical systems.

The formalization process was completed efficiently with minimal human coding and supervision.

The entire development is publicly archived, providing transparency and reproducibility.

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.