Formalisation semi-autonome de l'équilibre de Vlasov-Maxwell-Landau
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Auteurs: Vasily Ilin
cs.AI
Résumé
Nous présentons une formalisation complète dans Lean 4 de la caractérisation de l'équilibre pour le système de Vlasov-Maxwell-Landau (VML), qui décrit le mouvement d'un plasma chargé. Ce projet illustre la boucle complète de recherche mathématique assistée par IA : un modèle de raisonnement IA (Gemini DeepThink) a généré la preuve à partir d'une conjecture, un outil de codage agentique (Claude Code) l'a traduite en Lean à partir d'invites en langage naturel, un prouveur spécialisé (Aristote) a clos 111 lemmes, et le noyau Lean a vérifié le résultat. Un seul mathématicien a supervisé le processus sur 10 jours pour un coût de 200 dollars, sans écrire une seule ligne de code.
L'intégralité du processus de développement est publique : les 229 invites humaines et les 213 commits git sont archivés dans le dépôt. Nous rapportons des enseignements détaillés sur les modes d'échec de l'IA – la dérive des hypothèses, les bugs d'alignement des définitions, les comportements d'évitement des agents – et sur ce qui a fonctionné : la séparation preuve abstraite/concrète, l'auto-révision contradictoire, et le rôle crucial de la revue humaine des définitions clés et des énoncés de théorèmes. Il est à noter que la formalisation a été achevée avant la version finale de l'article mathématique correspondant.
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.