{"id":"arxiv/2609.32561","url":"https://arxiv.org/abs/2609.32561","tags":["math.AP","cs.LO"],"score":0,"title":"Formalising Linear Elliptic PDE Theory in Lean 4","domain":"math.AP","source":"arxiv","authors":["Alejandro José Soto Franco","Kobe Marshall-Stevens"],"reviews":0,"subject":"math.AP","summary":"We formalise in Lean 4, on top of Mathlib, the solvability of the Dirichlet problem for second-order linear elliptic operators in divergence form. The machine-verified results, with no sorry in the development, include the Poincaré inequality, the existence of weak solutions by the Lax-Milgram theorem, Rellich-Kondrachov compactness, the Fredholm alternative, the spectral theorem, interior regularity estimates, and the Sobolev embedding theorem. From these results we obtain a formalisation of classical solvability for sufficiently regular coefficients and data. Our Lean library includes a…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-26","reactions":{}}