Formalising Linear Elliptic PDE Theory in Lean 4

Alejandro José Soto Franco, Kobe Marshall-Stevens

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, wit…