Showing 2026Show all
2 papers · 1 filter
math.AP2026
Formalising Linear Elliptic PDE Theory in Lean 4
Alejandro José Soto Franco, Kobe Marshall-Stevens
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, wit…
math.DG2026
Isoperimetry by stretching
Kobe Marshall-Stevens, Gongping Niu
We construct isoperimetric regions from separating hypersurfaces in closed manifolds. This yields isoperimetric boundaries exhibiting a wide variety of topological types and singul…