Erdős's diameter conjecture for separated distances fails in high dimensions

Erdős asked whether every $n$-point set in Euclidean space whose $\left(\genfrac{}{}{0px}{}{n}{2}\right)$ 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 $$\mathrm{diam}({\mathcal{X}}_q)\le (1-\frac{1}{{\pi }^2}+o(1))n^2\mathrm{.}$$ The proof is fully formalized in Lean 4.