Semigeautomatiseerde formalisering van het Vlasov-Maxwell-Landau-evenwicht
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Auteurs: Vasily Ilin
cs.AI
Samenvatting
Wij presenteren een volledige Lean 4-formalisering van de evenwichtskarakterisering in het Vlasov-Maxwell-Landau (VML) systeem, dat de beweging van geladen plasma beschrijft. Het project demonstreert de volledige, door AI ondersteunde onderzoekscyclus: een AI-redeneermodel (Gemini DeepThink) genereerde het bewijs vanuit een vermoeden, een agent-gebaseerd codeergereedschap (Claude Code) vertaalde het naar Lean op basis van prompts in natuurlijke taal, een gespecialiseerde prover (Aristotle) sloot 111 lemma's af, en de Lean-kernel verifieerde het resultaat. Een enkele wiskundige begeleidde het proces gedurende 10 dagen tegen een kostenpost van \$200, zonder ook maar één regel code te schrijven.
Het gehele ontwikkelproces is openbaar: alle 229 menselijke prompts en 213 git-commits zijn gearchiveerd in de repository. Wij rapporteren gedetailleerde lessen over AI-faalmodi – hypothese-creep, definitie-uitlijningsbugs, vermijdingsgedrag van agents – en over wat wel werkte: de splitsing tussen abstracte/concrete bewijzen, adversariële zelf-evaluatie, en de cruciale rol van menselijke beoordeling van sleuteldefinities en stellingen. Opmerkelijk is dat de formalisering werd voltooid voordat de definitieve versie van het bijbehorende wiskundige artikel was afgerond.
English
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.