Halbautonome Formalisierung des Vlasov-Maxwell-Landau-Gleichgewichts
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Autoren: Vasily Ilin
cs.AI
Zusammenfassung
Wir präsentieren eine vollständige Lean-4-Formalisierung der Gleichgewichtscharakterisierung im Vlasov-Maxwell-Landau (VML)-System, welches die Bewegung von geladenem Plasma beschreibt. Das Projekt demonstriert den vollständigen KI-gestützten mathematischen Forschungszyklus: Ein KI-Modell für logisches Schließen (Gemini DeepThink) generierte den Beweis aus einer Vermutung, ein agentenbasiertes Codierwerkzeug (Claude Code) übersetzte ihn anhand von natürlichsprachlichen Prompts in Lean, ein spezialisierter Beweiser (Aristotle) schloss 111 Lemmata ab, und der Lean-Kernel verifizierte das Ergebnis. Ein einzelner Mathematiker überwachte den Prozess über 10 Tage hinweg zu einem Preis von 200 US-Dollar, ohne eine einzige Codezeile zu schreiben.
Der gesamte Entwicklungsprozess ist öffentlich einsehbar: Alle 229 menschlichen Prompts und 213 Git-Commits sind im Repository archiviert. Wir berichten detailliert über Erkenntnisse zu KI-Fehlverhalten – Hypotheseenkrement, Definitionsabgleichsfehler, Vermeidungsverhalten von Agenten – und darüber, was funktioniert hat: die Aufteilung in abstrakte/konkrete Beweise, adversarische Selbstüberprüfung und die entscheidende Rolle menschlicher Überprüfung von Schlüsseldefinitionen und Theoremen. Bemerkenswerterweise wurde die Formalisierung abgeschlossen, bevor der endgültige Entwurf des entsprechenden mathematischen Papers fertiggestellt war.
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.