Papers With

← All papers
First page of Formalising Linear Elliptic PDE Theory in Lean 4

Formalising Linear Elliptic PDE Theory in Lean 4

Alejandro José Soto Franco, Kobe Marshall-Stevens

math.AP Sep 26, 2026 · v1 cs.LO
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Formalises in Lean 4 on Mathlib the solvability of the Dirichlet problem for second-order linear elliptic operators, with a self-contained Sobolev space theory.
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.
Problem

Partial differential equation theory has seen little formalisation in interactive theorem provers. The solvability of the Dirichlet problem for second-order linear elliptic operators in divergence form had not been machine-verified.

Approach

The authors build a Lean 4 library on top of Mathlib, developing a self-contained theory of Sobolev spaces realised as weak-derivative Hilbert spaces (L^2 functions with their L^2 gradients). Weak solvability is obtained via coercivity from the Poincaré inequality and Mathlib's Lax-Milgram theorem. Compactness is proved through the Fréchet-Kolmogorov criterion, and regularity via a bootstrap in half-steps and Sobolev embedding. Each prose statement is paired with the named Lean declaration that proves it.

Results

The development, with no sorry and depending only on propext, Classical.choice and Quot.sound, formalises the Poincaré inequality, existence of weak solutions, Rellich-Kondrachov compactness, the Fredholm alternative, the spectral theorem, interior regularity estimates, and the Sobolev embedding theorem, yielding classical solvability for regular data. The discharge ratio of the claimed results is 1.