Summary (Overview)

• This paper presents a comprehensive formalisation in Lean 4 of the solvability of the Dirichlet problem for second-order linear elliptic operators in divergence form, built on top of Mathlib.
• The machine-verified results (with no sorry in the development) include the Poincaré inequality, Lax–Milgram theorem, Rellich–Kondrachov compactness, Fredholm alternative, spectral theorem, interior regularity estimates, and the Sobolev embedding theorem.
• The authors develop a self-contained theory of Sobolev spaces independently of existing formalisations, using a weak-derivative Hilbert space approach.
• The library achieves classical solvability for sufficiently regular coefficients and data, with every prose statement associated with a named machine-checked Lean declaration.
• The development was assisted by language models (Claude Opus 4.5 and 5) used as agents, though no model output forms part of the trusted proof object—the Lean kernel checks every proof term.

Introduction and Theoretical Foundation

The paper addresses the formalisation of partial differential equation (PDE) theory in interactive proof assistants, an area still in its early stages. While mathematical analysis has recently come within reach of proof assistants, PDE theory formalisation lags behind. Previous work includes interior De Giorgi–Nash–Moser regularity theory in Lean 4 [AK26], Gagliardo–Nirenberg–Sobolev inequality formalisations [DM24], and Schwartz functions and tempered distributions [Dol25].

The mathematical foundation concerns second-order linear partial differential operators $L$ in divergence form with coefficients $a^{ij}, b^i, c \in L^\infty(\Omega)$:

$$Lu = -\sum_{j=1}^{n} D_j\left(\sum_{i=1}^{n} a^{ij} D_i u\right) + \sum_{i=1}^{n} b^i D_i u + c u \tag{1}$$

The operator is uniformly elliptic if there exist constants $0 < \lambda \leq \Lambda < \infty$ such that for each $\xi \in \mathbb{R}^n$:

$$0 < \lambda |\xi|^2 \leq \sum_{i,j=1}^{n} a^{ij}(x)\xi_i \xi_j \leq \Lambda |\xi|^2 \tag{2}$$

The Dirichlet problem is:

$$\begin{cases} Lu = f & \text{in } \Omega, \\ u = 0 & \text{on } \partial\Omega. \end{cases} \tag{3}$$

A weak solution $u \in H^1_0(\Omega)$ satisfies:

$$B[u, v] = \langle f, v \rangle_{L^2(\Omega)} \quad \text{for all } v \in H^1_0(\Omega) \tag{4}$$

where the bilinear form is:

$$B[u, v] = \sum_{i,j=1}^{n} \int_\Omega \left(a^{ij} D_i u D_j v + b^i (D_i u) v + c uv\right) \tag{5}$$

The approach follows the two-stage classical strategy: first obtain weak solutions via functional-analytic methods (Lax–Milgram and Fredholm alternative), then show via interior regularity estimates and Sobolev embedding that weak solutions are classical when coefficients and data are sufficiently regular.

Methodology

Formalisation Framework

The formalisation assigns one of four statuses to each proof obligation:

• Discharged: established by a machine-checked Lean proof term
• Warranted: deferred to a located external source
• Routine: relies on shared mathematical competence
• Open: no justification given

Acceptance criteria are mechanical: the full development must build from a clean clone with no sorry and no warnings, the environment linter must pass, and #print axioms must report exactly the three standard Lean core axioms (propositional extensionality, axiom of choice, and quotient soundness).

Library Architecture

The library consists of three layers:

1. Weak-derivative Sobolev layer: Sobolev spaces realised as weak-derivative Hilbert spaces, where a member is an $L^2$ function together with its $L^2$ gradients. The ambient space is $L^2(\Omega) \times (L^2(\Omega))^n$, encoded as PiLp 2 over Fin (n + 1). The space $H^1_0(\Omega)$ is the topological closure of test-function graphs.

2. Poincaré reduction layer: The Poincaré constant is derived from one-dimensional estimates. Two key lemmas are formalised:

   • Lemma 1 (One-dimensional Cauchy–Schwarz): $\left(\int_a^b f(t)g(t)\,dt\right)^2 \leq \left(\int_a^b f(t)^2\,dt\right)\left(\int_a^b g(t)^2\,dt\right)$
   • Lemma 2 (One-dimensional Poincaré): $\int_a^b u(t)^2\,dt \leq \frac{(b-a)^2}{2}\int_a^b u'(t)^2\,dt$

3. Sobolev embedding layer: Provides passage from equivalence classes to pointwise-defined functions, using Gagliardo–Nirenberg–Sobolev and Morrey inequalities.

Key Formalised Theorems

Theorem 1 (Poincaré inequality): For bounded $\Omega \subseteq \mathbb{R}^n$, there exists $C_P \geq 0$ such that $\|u\|_{L^2(\Omega)} \leq C_P \|\nabla u\|_{L^2(\Omega)}$ for all $u \in H^1_0(\Omega)$.

Theorem 2 (Lax–Milgram): For a Hilbert space $H$ with bounded coercive bilinear form $B$ satisfying $B[u,u] \geq \beta\|u\|^2_H$ for $\beta > 0$, and $f \in H^*$, there is a unique $u \in H$ with $B[u,v] = \langle f, v\rangle$ for all $v \in H$.

Theorem 3 (Gårding inequality): With $\gamma = \lambda/2 + \|c\|_{L^\infty(\Omega)} + n(\max_i\|b^i\|_{L^\infty(\Omega)})^2/(2\lambda)$:

$$\frac{\lambda}{2}\|u\|^2_{H^1_0(\Omega)} \leq B[u,u] + \gamma\|u\|^2_{L^2(\Omega)}$$

Theorem 5 (Fredholm alternative): For bounded measurable $\Omega$ and uniformly elliptic $L$, either the homogeneous problem has a non-zero weak solution, or for every $f \in H^{-1}(\Omega)$, the problem $Lu = f$ has a unique weak solution.

Theorem 10 (Sobolev embedding): For $n \geq 2$, bounded open $\Omega$ with $C^1$ boundary, $p \in [1, \infty)$, $k \in \mathbb{N}$, $u \in W^{k,p}(\Omega)$:

1. If $k < n/p$, then $u \in L^q(\Omega)$ with $1/q = 1/p - k/n$
2. If $k > n/p$, then $u \in C^{k-1-\lfloor n/p\rfloor,\gamma}(\Omega)$ with $\gamma = \begin{cases} \text{any value in } (0,1), & n/p \in \mathbb{N} \\ \lfloor n/p\rfloor - n/p + 1, & n/p \notin \mathbb{N} \end{cases}$

Theorem 11 (Interior $H^2$ regularity): If $a^{ij} \in C^1(\Omega)$, $b^i, c \in L^\infty(\Omega)$, $f \in L^2(\Omega)$, and $u \in H^1(\Omega)$ is a weak solution, then $u \in H^2_{\text{loc}}(\Omega)$ with $\|u\|_{H^2(V)} \leq C(\|f\|_{L^2(\Omega)} + \|u\|_{L^2(\Omega)})$ for each open $V \Subset \Omega$.

Theorem 12 (Higher interior regularity): With $a^{ij}, b^i, c \in C^{m+1}(\Omega)$ and $f \in H^m(\Omega)$, a weak solution satisfies $u \in H^{m+2}_{\text{loc}}(\Omega)$ with appropriate estimates.

Theorem 13 (Infinite differentiability): With $C^\infty$ coefficients and data, weak solutions have smooth representatives.

Empirical Validation / Results

The paper provides detailed Lean statements for each theorem. Key results include:

Corollary 1 (Poisson equation): For every $f \in H^{-1}(\Omega)$, there is a unique $u \in H^1_0(\Omega)$ with $\sum_{i=1}^n \langle \partial_i u, \partial_i v\rangle_{L^2(\Omega)} = f(v)$ for every $v \in H^1_0(\Omega)$.

Theorem 4 (Existence I): For bounded $\Omega$, uniformly elliptic $L$ with $b = 0$ and $c \geq 0$, the problem (3) has a unique weak solution with $\|u\|_{H^1_0(\Omega)} \leq \alpha^{-1}\|f\|_{L^2(\Omega)}$ where $\alpha = \lambda/(1 + C_P^2)$.

Theorem 7 (Variational principle): For symmetric coercive $B$ with compact embedding, $\lambda_1 = \inf\{B[u,u] : \|u\|_{L^2(\Omega)} = 1\} > 0$ is attained, and the minimiser satisfies $B[u,v] = \lambda_1\langle u,v\rangle_{L^2(\Omega)}$ for all $v$.

Theorem 8 (Spectrum of compact operator): For compact operator $K$ on infinite-dimensional real Hilbert space, zero lies in the spectrum, non-zero spectrum consists of countably many eigenvalues with finitely many satisfying $|\mu| \geq \delta$ for each $\delta > 0$.

Corollary 3 (Classical solvability): With $C^1$ principal coefficients, $W^{k,\infty}$ coefficients, and $H^k$ data for all $k$, the Dirichlet problem has a unique weak solution with a smooth representative satisfying $Lu = f$ pointwise almost everywhere.

The discharge ratio (fraction of claimed results established by named Lean declarations) is 1—every claimed result is discharged by a named declaration with no warranted, routine, or open steps.

Theoretical and Practical Implications

1. Mathematical significance: The formalisation covers the complete chain from weak solvability through regularity to classical solvability, representing a substantial portion of modern linear elliptic PDE theory placed on machine-verified footing.

2. Technical contributions:

   • The Poincaré inequality is derived from one-dimensional estimates alone, giving explicit constants
   • Compactness of the embedding is proved via the Fréchet–Kolmogorov criterion
   • The declaration for Theorem 12 takes weaker hypotheses ($a^{ij} \in W^{m+1,\infty}$, $b^i, c \in W^{m,\infty}$) than the classical $C^{m+1}$ statement
   • Variational construction of eigenvalues is independent of the spectral theorem and extends to semilinear equations

3. Practical implications: The library provides reusable infrastructure for further formalisation work in PDE theory, including boundary regularity, Harnack's inequality, and Schauder theory.

Conclusion

The paper successfully formalises the classical solvability of the Dirichlet problem for linear elliptic PDEs in divergence form using Lean 4 and Mathlib. Key achievements include:

• A self-contained weak-derivative Sobolev space theory
• Complete proofs of existence, uniqueness, and regularity theorems
• Explicit correspondence between prose statements and machine-checked Lean declarations

Future directions identified by the authors include:

• Removing the $C^1$ hypothesis on principal coefficients (requires identifying $W^{1,\infty}$ functions with Lipschitz representatives)
• Boundary regularity theory (closest to completion, with half-ball geometry and tangential difference quotients already formalised)
• Harnack's inequality (requires Moser iteration, not yet in the library)
• Schauder theory (Campanato's characterisation proved but unused)
• Completion of eigenvalue theory (positivity and simplicity of $\lambda_1$ require strong maximum principle)
• Boundary integration by parts against surface measure (requires divergence theorem on manifolds with boundary, as in [CLQ26])

The library is openly available at https://github.com/alejandro-soto-franco/EllipticPDE, pinned at commit da8dd98, built with Lean 4 v4.31.0-rc1 and Mathlib commit 542645a.