{"id":"arxiv/2605.20527","url":"https://arxiv.org/abs/2605.20527","tags":["math.FA","math.CA"],"score":0,"title":"$L^2$-Stability for STFT phase retrieval","domain":"math.FA","source":"arxiv","authors":["Susanna Bertolini","Jaume de Dios Pont","Ben Pineau","Mitchell A. Taylor","João P. G. Ramos"],"reviews":0,"subject":"math.FA","summary":"We prove that the short-time Fourier transform with Gaussian window performs $L^2$-local stable phase retrieval at the constant function. The proof involved significant interplay between mathematicians and LLMs. An autoformalization in Lean 4 of an extension of our result to $L^2$-local stable phase retrieval for all Hermite windows and all elements in the finite span of the canonical basis vectors is also presented.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-05-19","reactions":{}}