A case study, not a new theorem: the authors recount how they combined LLM-generated mathematics with Lean verification in Banach lattice theory and phase retrieval.
Stable Phase Retrieval for Spans of Independent Random Variables
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
We prove that, after $L^2$ normalization, stable phase retrieval holds over the $L^2$-spans of independent real-valued centered random variables if and only if all but possibly one coordinate satisfies a uniform two-sided $L^1$ bound. This provides a complete characterization of stable phase retrieval for such subspaces, building upon the pioneering work of Calderbank--Daubechies--Freeman--Freeman and confirming the conjectured characterization communicated to us by those authors. We provide two different proofs of this fact, both based on a decomposition of the $\ell^2$-coefficients of each random variable. The first is a compactness proof, which makes use of the infinite divisibility of limit laws of tail sums. The second is a quantitative proof, which substitutes the compactness step with an explicit dichotomy based on anticoncentration estimates of Sperner type. This latter proof was partially LLM generated based on the ideas in the first proof and a considerable amount of guidance by the authors. An autoformalization of our main result in Lean 4 is also provided, following the ideas in the quantitative proof.
citation-role summary
citation-polarity summary
fields
math.FA 1years
2026 1verdicts
UNVERDICTED 1roles
background 1polarities
unclear 1representative citing papers
citing papers explorer
-
Banach lattices and phase retrieval: A case study for the use of AI in mathematics
A case study, not a new theorem: the authors recount how they combined LLM-generated mathematics with Lean verification in Banach lattice theory and phase retrieval.