Skip to content
DraconiticResearch
Search Sources API
197,768 studies31 sourcesUpdated 15 min ago
PreprintCC BY 4.0arXiv

Formalising Linear Elliptic PDE Theory in Lean 4

  • Alejandro José Soto Franco
  • Kobe Marshall-Stevens
Open at sourcePDFDOICite

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.

Related

  1. Formalising John Dee's Monas Hieroglyphica in Lean 4
    Ivan Matychyn
    arXivPreprintarXiv licenceFull textGeneral mathematicsarXiv
  2. Formalizing Fefferman's Official Periodic Navier-Stokes Problem (B) in Lean 4: Global Linear Strain Exclusion on T3, Biot-Savart Direction Depletion Identities, and Conditional Reductions via Beale-Kato-Majda
    Benjamin Frohman
    Zenodo (CERN European Organization for Nuclear Research)PreprintLicence not stated5 citedGeneral mathematicsOpenAlex
  3. Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory
    Fubin Yan, Ruxuan Dong, Ruoxuan Shi +2
    arXivPreprintCC BY 4.0Full textGeneral mathematicsarXiv
  4. On Polynomial Complex Hessian Equations I: Non-Linear Non-Spectral Elliptic Hessian Equations on Riemannian Manifolds
    Rémi Delloque
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsGeometry & topologyarXiv
  5. Isolated singularities of certain quasi-linear elliptic inequalities II
    Shiguang Ma, Shengyang Zang
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsarXiv

Cite

BibTeXRIS
BibTeX
@misc{franco2026formalising,
  title = {{Formalising Linear Elliptic PDE Theory in Lean 4}},
  author = {Alejandro José Soto Franco and Kobe Marshall-Stevens},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.32561},
  eprint = {2609.32561},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.32561},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Formalising Linear Elliptic PDE Theory in Lean 4
AU  - Alejandro José Soto Franco
AU  - Kobe Marshall-Stevens
PY  - 2026
DA  - 2026/09/26
PB  - arXiv
DO  - 10.48550/arxiv.2609.32561
UR  - https://arxiv.org/abs/2609.32561
AB  - 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.
ER  -