Erd\H{o}s's diameter conjecture for separated distances fails in high dimensions

TL;DR

The paper disproves Erdős's conjecture by constructing high-dimensional point sets with large mutual distances but smaller than expected diameter, formalized in Lean 4.

Contribution

It provides explicit constructions in high dimensions that counter Erdős's diameter conjecture, with formal proof in Lean 4.

Findings

Constructed point sets with mutual distances at least 1

Diameter of constructed sets is less than (1 - 1/π^2 + o(1)) n^2

Disproved a longstanding conjecture in Euclidean geometry

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.