The Spherical Cap Conjecture asserts that spherical caps are the only constant mean curvature disks immersed in R^3 with H≠0 and circular boundary. This had remained open in its immersed form.

The proof uses the Lawson correspondence in quaternionic first-order form and a flux formula. Along the boundary the developing equation reduces to an ODE in S^3, and a boundary lemma characterizes when the developing map closes up, forcing constant contact angle. Nitsche's line-of-curvature argument then yields the embedded spherical cap. The analytic boundary lemma (Lemma 3.1) was formalized in Lean 4 with Mathlib, proving both implications under the stated analytic hypotheses.

Every smooth immersed disk in R^3 with nonzero constant mean curvature, regular up to the boundary and mapping its boundary diffeomorphically onto a circle, is an embedded spherical cap. The Lean formalization covers the boundary lemma but not the geometric reduction or final surface classification.