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

arXiv: https://arxiv.org/abs/2603.15929 · HTML: https://mlsanity.com/paper/2603.15929/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 30 references that are in the map.
- First posted on arXiv 16 Mar 2026.

## Builds on (most cited first, 7 of 7)

- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature](https://mlsanity.com/paper/2603.08139/) (2026)

## Built on by (most cited first, 9 of 9)

- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization](https://mlsanity.com/paper/2606.13925/) (2026)
- [A Formalization of the Mean-Field Derivation of the Vlasov Equation](https://mlsanity.com/paper/2607.08986/) (2026)
- [Workflow Closure Is Not Scientific Closure in Auto-Research Systems](https://mlsanity.com/paper/2605.26200/) (2026)
- [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [A Neural Score-Based Particle Method for the Vlasov-Maxwell-Landau System](https://mlsanity.com/paper/2603.25832/) (2026)
- [Benign Loss Landscapes Can Coexist with Worst-Case Hardness](https://mlsanity.com/paper/2609.13057/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.