Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.32561

Formalising Linear Elliptic PDE Theory in Lean 4

Alejandro José Soto Franco·Kobe Marshall-Stevens
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

math.APcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Alejandro José Soto Franco, Kobe Marshall-Stevens. 2026-09-26. Formalising Linear Elliptic PDE Theory in Lean 4. https://arxiv.org/abs/2609.32561

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Boundary Regularity for Fully Nonlinear Degenerate Elliptic Equations

This paper investigates fully nonlinear degenerate elliptic equations of the form $|Du|^γF(D^2u) = f$ with $γ>0$ {and $F(0)=0$}. Using a unified compactness and perturbation framework, we {establish} $C^1$ regularity on $C^{1,\mathrm{Dini}}$ domains and {$C^{1,α_0}$ regularity on $C^{1,α}$ domains}, {where $α_0=\min\{α,1/(1+γ)\}$}. {In addition}, we construct a counterexample to show that {$W^{2,δ}$ regularity does not hold for any $δ>0$}.

math.AP↗
arXiv2026

Localizing acoustic and electromagnetic waves in space and time

We study time-dependent acoustic and electromagnetic waves governed by the scalar wave equation or Maxwell's equations in a bounded three-dimensional domain. We establish the existence of time-dependent boundary excitations that can be prescribed on any open subset of the boundary of the domain such that the associated waves are strongly localized in space in the sense that they possess arbitrarily large norms in a given subdomain and on a given time-interval, while remaining arbitrarily small in any other given subdomain for all times. Similarly, we also show the existence of boundary data such that the associated waves are strongly localized in time in the sense that they possess arbitrarily large norms in a given subdomain and on a given time-interval, while remaining arbitrarily small on the same subdomain but on any other prescribed time-interval. In case that we have access to the possibly inhomogeneous coefficients in the wave equation or in the Maxwell system, we also give explicit constructions to obtain boundary data that generate these localized waves, and we comment on possible applications.

math.AP↗
arXiv2026

Brunn-Minkowski Inequality for p-Harmonic Measures

We prove a Brunn--Minkowski inequality for a functional associated with p-harmonic measures for $1<p<n+1$, on a class of convex domains satisfying suitable conditions. Under an additional first-variation assumption, we also prove uniqueness up to dilation about the origin for the corresponding Minkowski problem. We also study geometric conditions involving level sets, support functions, and Gaussian curvature for the problem with a fixed inner body.

math.AP↗