{"id":"arxiv:2609.32561","kind":"preprint","title":"Formalising Linear Elliptic PDE Theory in Lean 4","authors":["Alejandro José Soto Franco","Kobe Marshall-Stevens"],"author_count":2,"year":2026,"published":"2026-09-26","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2609.32561","nct_id":null,"source_url":"https://arxiv.org/abs/2609.32561","archive_url":"https://space-kitty.com/papers/arxiv:2609.32561","updated":"2026-09-26","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2609.32561","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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["math.AP","cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}