Lean 4 formalization proves Singer's Sidon-set construction for every prime power and builds a library that yields unconditional two-sided bounds h(N)=Θ(√N) plus a conditional route to the full Erdős Problem 30 asymptotic.
Erd\H{o}s's diameter conjecture for separated distances fails in high dimensions
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
abstract
Erd\H{o}s asked whether every $n$-point set in Euclidean space whose $\binom{n}{2}$ pairwise distances are mutually at least $1$ apart must have diameter at least $(1+o(1))n^2$. We disprove this statement by constructing for every prime power $q$ a set $\mathcal X_q\subset \mathbb R^{q^2+q}$ of $n=q+1$ points such that all pairwise distances in $\mathcal X_q$ are mutually at least $1$ apart, while $$\operatorname{diam}(\mathcal X_q)\le\Bigl(1-\frac{1}{\pi^2}+o(1)\Bigr)n^2.$$ The proof is fully formalized in Lean 4.
years
2026 2verdicts
ACCEPT 2representative citing papers
Stable phase retrieval holds for L2-spans of independent centered real random variables iff all but at most one coordinate obeys a uniform two-sided L1 bound.
citing papers explorer
-
Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
Lean 4 formalization proves Singer's Sidon-set construction for every prime power and builds a library that yields unconditional two-sided bounds h(N)=Θ(√N) plus a conditional route to the full Erdős Problem 30 asymptotic.
-
Stable Phase Retrieval for Spans of Independent Random Variables
Stable phase retrieval holds for L2-spans of independent centered real random variables iff all but at most one coordinate obeys a uniform two-sided L1 bound.