Formal verification of solving classical linear elliptic PDEs in Lean
Formalising Linear Elliptic PDE Theory in Lean 4
Logic in Computer Science
Summary
Solving certain types of differential equations, called linear elliptic partial differential equations (PDEs), is important in physics and engineering. The paper describes how the authors used a computer proof assistant called Lean 4 to rigorously build and check a complete mathematical theory behind solving these equations. Their formalized math ensures no steps are missing or incorrect and includes key results like existence and uniqueness of solutions. This work helps people trust and build on complex math foundations using computers.
What this means in practice
- •For formal methods engineers: Use a verified Lean 4 library for linear elliptic PDE theory to build provably correct numerical solvers and verified scientific computing tools.
- •For computational engineers: Improve confidence in PDE solver implementations by referencing a fully formalized mathematical foundation in Lean 4 for second-order linear elliptic PDEs.
Authors
Alejandro José Soto Franco, Kobe Marshall-Stevens
Abstract
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 self-contained theory of Sobolev spaces developed independently of existing formalisations. Throughout the paper we associate each prose statement with the named machine-checked Lean declaration that discharges it.