{"id":"arxiv/2609.16801","url":"https://arxiv.org/abs/2609.16801","tags":["math.AP"],"score":0,"title":"Formalization of Landau damping in the Vlasov--Poisson equations in Lean","domain":"math.AP","source":"arxiv","authors":["Jacob Bedrossian"],"reviews":0,"subject":"math.AP","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-15","reactions":{}}