{"id":"arxiv/2604.15305","url":"https://arxiv.org/abs/2604.15305","tags":["math.CO","math.MG"],"score":0,"title":"Erdős's diameter conjecture for separated distances fails in high dimensions","domain":"math.CO","source":"arxiv","authors":["Boon Suan Ho"],"reviews":0,"subject":"math.CO","summary":"Erdő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}{π^2}+o(1)\\Bigr)n^2.$$ The proof is fully formalized in Lean 4.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-16","reactions":{}}