Formalización Semiautónoma del Equilibrio de Vlasov-Maxwell-Landau
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Autores: Vasily Ilin
cs.AI
Resumen
Presentamos una formalización completa en Lean 4 de la caracterización del equilibrio en el sistema de Vlasov-Maxwell-Landau (VML), que describe el movimiento de un plasma cargado. El proyecto demuestra el ciclo completo de investigación matemática asistida por IA: un modelo de razonamiento de IA (Gemini DeepThink) generó la demostración a partir de una conjetura, una herramienta de codificación agente (Claude Code) la tradujo a Lean a partir de instrucciones en lenguaje natural, un demostrador especializado (Aristotle) cerró 111 lemas, y el núcleo de Lean verificó el resultado. Un único matemático supervisó el proceso durante 10 días con un coste de 200 dólares, sin escribir una sola línea de código.
Todo el proceso de desarrollo es público: las 229 instrucciones humanas y los 213 commits de git están archivados en el repositorio. Informamos lecciones detalladas sobre los modos de fallo de la IA —como la deriva de hipótesis, los errores de alineación de definiciones y los comportamientos de evitación de los agentes— y sobre lo que funcionó: la división abstracta/concreta de la demostración, la autorrevisión adversarial y el papel crucial de la revisión humana de las definiciones clave y los enunciados de los teoremas. Cabe destacar que la formalización se completó antes de que terminara el borrador final del artículo de matemáticas correspondiente.
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.