Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
This work demonstrates a semi-autonomous AI pipeline for mathematical formalization, potentially accelerating proof verification in plasma physics and related fields, though it is incremental in applying existing AI tools to a specific domain.
The researchers tackled the problem of formalizing the equilibrium characterization in the Vlasov-Maxwell-Landau system using AI-assisted tools, achieving a complete Lean 4 formalization with 111 lemmas closed and verification by the Lean kernel, supervised by a single mathematician over 10 days at a cost of $200 without writing code.
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.