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

Computer Science > Artificial Intelligence [Submitted on 16 Mar 2026] Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium Vasily Ilin 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. Comments: 11 figures Subjects: Artificial Intelligence (cs.AI); Analysis of PDEs (math.AP); Logic (math.LO) MSC classes: 68V15 (primary), 68T01, 35Q83, 82D10 (secondary) ACM classes: I.2.3; F.4.1; J.2 Cite as: arXiv:2603.15929 [cs.AI]   (or arXiv:2603.15929v1 [cs.AI] for this version)   https://doi.org/10.48550/arXiv.2603.15929 Focus to learn more Submission history From: Vasily Ilin [view email] [v1] Mon, 16 Mar 2026 21:21:53 UTC (1,754 KB) Access Paper: HTML (experimental) view license Current browse context: cs.AI < prev   |   next > new | recent | 2026-03 Change to browse by: cs math math.AP math.LO References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)