# The hot spots conjecture for simply connected planar domains

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Strict hot spots and absence of interior critical points on smooth simply connected planar domains](../../preprints/Strict-hot-spots-and-absence-of-interior-critical-points-on-smooth-simply-connected-planar-domains-September-24-2026/main.pdf)

## Scope

The strict hot-spots conjecture asks whether extrema of a first nonconstant Neumann eigenfunction occur only on the boundary. The formalization proves the stronger interior statement on every nonempty smooth bounded simply connected planar domain: every nonzero eigenfunction in the first positive Neumann eigenspace has nonvanishing gradient throughout the interior. Consequently all global maxima and minima lie on the boundary. The conclusion applies to every eigenfunction even when the eigenvalue is multiple.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Strict hot spots and absence of interior critical points | [HotSpots.lean](../ComparatorChallenges/HotSpots.lean) |