KI-gestützte Formalisierung des Vlasov‑Maxwell‑Landau‑Equilibriums in Lean 4

In einer kürzlich veröffentlichten Arbeit auf arXiv wurde die vollständige Formalisierung der Gleichgewichtskarakterisierung des Vlasov‑Maxwell‑Landau‑Systems in der Programmiersprache Lean 4 vorgestellt. Das System beschreibt die Bewegung geladener Plasmen und ist ein zentrales Modell in der theoretischen Plasma‑Physik.

Der gesamte Forschungszyklus wurde von künstlicher Intelligenz unterstützt. Das KI‑Modell Gemini DeepThink erstellte zunächst einen Beweis aus einer gegebenen Vermutung. Anschließend wandelte das agentische Codierungstool Claude Code die natürlichen Sprachbefehle in Lean‑Code um. Der spezialisierte Theoremprover Aristotle schloss 111 Lemmas ab, und der Lean‑Kernel verifizierte das Endergebnis. Ein einzelner Mathematiker beaufsichtigte den Vorgang über zehn Tage, verfasste keine Codezeilen und investierte 200 US Dollar.

Alle 229 menschlichen Eingaben und 213 Git‑Commits sind öffentlich zugänglich. Die Autoren berichten über typische KI‑Fehlermuster wie Hypothesen‑Verzerrung, Definition‑Abstimmungsfehler und Vermeidungsverhalten des Agenten. Gleichzeitig betonen sie, welche Ansätze erfolgreich waren: die Trennung von abstrakten und konkreten Beweisen, ein adversariales Selbst‑Review und die entscheidende Rolle menschlicher Kontrolle bei Schlüsseldefinitionen und Theorem‑Aussagen. Interessanterweise wurde die Formalisierung bereits abgeschlossen, bevor der endgültige Entwurf der zugehörigen wissenschaftlichen Publikation fertiggestellt war.