The stability of short-time Fourier transform (STFT) phase retrieval is an open problem: can one stably recover a function from the magnitude of its STFT? Prior results did not establish L^2-local stable phase retrieval for the Gaussian window at the constant function.

The authors prove that the STFT with Gaussian window performs L^2-local stable phase retrieval at the constant function. The proof reduces the problem to a coercivity estimate in the Fock space, proceeding through a local reduction (in reproducing kernel Hilbert spaces) and an orthogonal reduction. An autoformalization in Lean 4 extends the result to all Hermite windows and all elements in the finite span of the canonical basis vectors. The collaboration involved significant interplay between mathematicians and LLMs, with conclusions at each step Lean-verified before the LLMs were prompted to generalize further.

The main theorem establishes an absolute constant C such that the stability inequality holds with explicit bounds. The Lean verification covers the generalized Theorem 1.5 for all Hermite windows in arbitrary dimension d, with the full code available at github.com/susannabertolini/PhaseRetrieval.