Formalizzazione Semi-Autonoma dell'Equilibrio di Vlasov-Maxwell-Landau
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Autori: Vasily Ilin
cs.AI
Abstract
Presentiamo una formalizzazione completa in Lean 4 della caratterizzazione dell'equilibrio nel sistema di Vlasov-Maxwell-Landau (VML), che descrive il moto del plasma carico. Il progetto dimostra l'intero ciclo di ricerca matematica assistita dall'IA: un modello di ragionamento IA (Gemini DeepThink) ha generato la dimostrazione a partire da una congettura, uno strumento di codifica agentico (Claude Code) l'ha tradotta in Lean a partire da prompt in linguaggio naturale, un dimostratore specializzato (Aristotele) ha chiuso 111 lemmi e il kernel di Lean ha verificato il risultato. Un singolo matematico ha supervisionato il processo in 10 giorni a un costo di 200 dollari, senza scrivere una sola riga di codice.
L'intero processo di sviluppo è pubblico: tutti i 229 prompt umani e i 213 commit git sono archiviati nel repository. Riferiamo lezioni dettagliate sulle modalità di fallimento dell'IA – deriva delle ipotesi, bug di allineamento delle definizioni, comportamenti di elusione degli agenti – e su ciò che ha funzionato: la divisione della dimostrazione in astratto/concreto, la revisione avversariale e il ruolo cruciale della revisione umana delle definizioni chiave e degli enunciati dei teoremi. È degno di nota che la formalizzazione sia stata completata prima della stesura finale del corrispondente articolo matematico.
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.