{"id":"arxiv/2603.15929","url":"https://arxiv.org/abs/2603.15929","tags":["cs.AI","math.AP","math.LO"],"score":0,"title":"Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium","domain":"cs.AI","source":"arxiv","authors":["Vasily Ilin"],"reviews":0,"subject":"cs.AI","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-03-16","reactions":{}}