Papers With

← All papers
First page of Formalization of Landau damping in the Vlasov–Poisson equations in Lean

Formalization of Landau damping in the Vlasov–Poisson equations in Lean

Jacob Bedrossian

math.AP Sep 15, 2026 · v1
formalization ai-agents analysis
Read PDF arXiv abstract Code
TL;DR
Formalizes Mouhot–Villani's nonlinear Landau damping theorem for Vlasov–Poisson equations in Lean 4 using agentic LLM workflows.
Abstract
We present a formalization in Lean 4 of Mouhot and Villani's theorem on nonlinear Landau damping in $\mathbb T^d$ in all Gevrey regularity indices $s > 1/3$ for small backgrounds.
Problem

Nonlinear Landau damping in the Vlasov–Poisson equations is a fundamental plasma-physics phenomenon whose mathematical proof (Mouhot and Villani) is highly technical. The goal was to produce a machine-checked formalization of this theorem.

Approach

The full statement of the Mouhot–Villani theorem on nonlinear Landau damping in the torus for Gevrey regularity indices s>1/3 with small backgrounds was formalized in Lean 4. Agentic LLMs wrote all the Lean code, supplied only with sketch lecture notes. The workflow evolved to have agents first verify proofs in natural language (with symbolic tools such as SymPy) using a planner, formalizer, and auditor set of three agents before converting to Lean, building supporting infrastructure like Fourier analysis on cylinder domains.

Results

A Lean 4 formalization of the nonlinear Landau damping theorem was completed, with the code publicly available. The author reports practical advice on agentic AI formalization workflows for mathematicians.