Papers With

← All papers
First page of Erdős's diameter conjecture for separated distances fails in high dimensions

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

Boon Suan Ho

math.CO Apr 16, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
Disproof of an Erdős conjecture, fully formalized in Lean 4.
Abstract
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.
Problem

Erdos conjectured that every n-point set in Euclidean space whose pairwise distances are mutually at least 1 apart must have diameter at least (1+o(1))n^2. This conjecture was open in high dimensions.

Approach

The authors disprove the conjecture by constructing, for every prime power q, a set X_q in R^{q^2+q} of n=q+1 points with all pairwise distances mutually at least 1 apart and diameter at most (1 - 1/pi^2 + o(1))n^2. The construction uses Singer difference sets and cyclic profiles to achieve the separation property. The proof is fully formalized in Lean 4, providing machine-checked verification of the counterexample.

Results

The constructed point sets achieve diameter at most (1 - 1/pi^2 + o(1))n^2, which is strictly less than the conjectured (1+o(1))n^2 lower bound. This disproves Erdos's diameter conjecture for separated distances in high dimensions. The full proof is computer-verified in Lean 4.