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

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\mathrm{/}3$ for small backgrounds.