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

Boon Suan Ho

arxiv: 2604.15305 · v1 · submitted 2026-04-16 · 🧮 math.CO · math.MG

ErdH{o}s's diameter conjecture for separated distances fails in high dimensions

Boon Suan Ho This is my paper

Pith reviewed 2026-05-10 10:32 UTC · model grok-4.3

classification 🧮 math.CO math.MG

keywords Erdős diameter conjectureseparated point setsminimum distance 1finite field constructionhigh-dimensional Euclidean spaceLean formalization

0 comments

The pith

Erdős's conjecture that any n points with pairwise distances at least 1 must have diameter at least roughly n squared fails in high dimensions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs, for every prime power q, a set of q+1 points in Euclidean space of dimension q squared plus q such that every pair is separated by distance at least 1, yet the largest distance in the set is at most (1 minus 1 over pi squared plus little-o of 1) times (q plus 1) squared. This supplies an explicit counterexample to Erdős's question whether the diameter of any such separated n-point set must be asymptotically n squared. A reader would care because the construction shows that the conjectured lower bound on diameter can be beaten by a positive constant factor once the dimension is allowed to grow with n. The algebraic nature of the sets and their verification in Lean 4 make the disproof fully rigorous.

Core claim

For every prime power q there exists a set X_q subset R^{q^2 + q} with |X_q|=q+1 such that all pairwise distances are at least 1 and diam(X_q) ≤ (1 - 1/π² + o(1)) (q+1)^2.

What carries the argument

The algebraic construction of the point set X_q from the finite field F_q, which embeds into Euclidean space of dimension q^2 + q while controlling all pairwise distances.

If this is right

The conjectured diameter lower bound of (1+o(1))n² does not hold once dimension reaches q² + q for n = q+1.
A strict asymptotic improvement of order 1/π² in the diameter is realized by these finite-field point sets.
The Lean formalization confirms that the algebraic distances meet both the separation condition and the reduced-diameter bound at once.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar algebraic constructions might exist in dimensions growing more slowly with n and would strengthen the disproof.
The result indicates that high-dimensional geometry permits tighter control over the spread of separated point sets than low-dimensional geometry allows.
One could test whether the same 1/π²-factor improvement appears for other families of finite geometries.

Load-bearing premise

The explicit algebraic construction over the finite field F_q yields Euclidean distances that simultaneously satisfy the minimum-distance and diameter bounds.

What would settle it

Direct computation of all pairwise Euclidean distances in the constructed set for a small prime power such as q=2 or q=3, checking whether every distance is at least 1 while the largest is strictly less than (1 - 1/π²)(q+1)^2.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

A Lean-formalized algebraic construction gives an explicit counterexample to Erdős's diameter conjecture with a fixed-factor improvement.

read the letter

The main thing here is a machine-checked counterexample to Erdős's conjecture on the diameter of n-point sets with minimum distance 1. For every prime power q the authors build q+1 points in R^{q²+q} whose pairwise distances are at least 1 while the diameter is at most (1 - 1/π² + o(1)) n². That constant and the specific family of constructions do not appear in the cited prior work, so the result is new on that point. The Lean 4 formalization covers the distance verifications and the asymptotic bound directly from the geometry of the point set, which removes the usual worry about calculation errors in high-dimensional embeddings. The construction is explicit and parameter-free once q is fixed, and the formalization supplies reproducible evidence rather than an analytic estimate that could hide gaps. The soft spots are modest. The improvement is only a fixed factor, not something that grows with n, and the points sit in dimension roughly n², which is high but allowed by the conjecture statement. The o(1) term means the bound is not sharp for finite q, though that does not affect the disproof. No load-bearing step is left outside the formalization. This paper is for researchers in discrete geometry and geometric graph theory who care about extremal problems with unit distances. It is worth a serious referee because the central claim is both formally grounded and directly falsifies a known conjecture; the referee can focus on whether the constant can be improved or whether the construction extends beyond prime powers.

Referee Report

0 major / 2 minor

Summary. The paper disproves Erdős's conjecture that any n-point set in Euclidean space with all pairwise distances at least 1 must have diameter at least (1+o(1))n². It does so by constructing, for every prime power q, an explicit set X_q of n=q+1 points in R^{q²+q} such that all pairwise distances are ≥1 while diam(X_q) ≤ (1-1/π² + o(1))n². The construction is algebraic over the finite field F_q and the distance bounds (including all verifications) are fully formalized and machine-checked in Lean 4.

Significance. This supplies a counterexample to a long-standing conjecture of Erdős on the geometry of separated point sets. The result is significant because the construction is explicit, parameter-free, and the central claims (minimum-distance condition and asymptotic diameter bound) rest entirely on a machine-checked formalization rather than analytic estimates or unverified calculations. This eliminates the usual risk of algebraic or numerical errors in high-dimensional distance computations.

minor comments (2)

The precise rate at which the o(1) term tends to zero (or the range of q for which the diameter inequality is verified) is not stated explicitly in the abstract or introduction; adding this would clarify the asymptotic statement.
Notation for the finite-field construction (e.g., the embedding of F_q into R^{q²+q}) could be cross-referenced more explicitly to the Lean code for readers who wish to inspect the formalization.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. Their summary accurately captures the main result: an explicit algebraic construction over finite fields that yields a counterexample to Erdős's conjecture, with all distance bounds and verifications fully formalized in Lean 4.

Circularity Check

0 steps flagged

No significant circularity; explicit construction verified by formalization

full rationale

The paper's central result is an explicit algebraic construction of n=q+1 points in R^{q^2+q} for each prime power q, together with direct verification that all pairwise Euclidean distances are at least 1 while the diameter satisfies the stated bound. This verification is performed entirely inside a Lean 4 formalization whose sole content is the distance calculations on the constructed point set. No parameters are fitted, no self-citation supplies a load-bearing uniqueness theorem or ansatz, and the diameter bound is obtained by evaluating the geometry of the given coordinates rather than by redefinition or statistical forcing. The derivation chain is therefore self-contained and externally checkable.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The argument relies on standard properties of finite fields and Euclidean norms; no free parameters are fitted to data and no new entities are postulated.

axioms (1)

standard math Vector space structure and inner-product geometry over finite fields of prime-power order
Used to define the point set X_q inside R^{q²+q} and to compute pairwise distances.

pith-pipeline@v0.9.0 · 5419 in / 1288 out tokens · 85285 ms · 2026-05-10T10:32:46.255463+00:00 · methodology

discussion (0)

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
math.CO 2026-05 accept novelty 8.0 full

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.
Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
math.CO 2026-05 accept novelty 6.0 full

Lean 4 formalization proves existence of a Sidon set of cardinality p+1 modulo p^2+p+1 for every prime p, plus reusable additive-combinatorics infrastructure and a conditional reduction toward Erdős Problem 30.

Reference graph

Works this paper leans on

8 extracted references · 8 canonical work pages · cited by 1 Pith paper

[1]

Bloom,Erdős Problems,https://www.erdosproblems.com

Thomas F. Bloom,Erdős Problems,https://www.erdosproblems.com

work page
[2]

Peter Brass, On the Erdős-diameter of sets,Discrete Mathematics150(1996), 415–419

work page 1996
[3]

Bollobás and A

Paul Erdős, Some unsolved problems, inCombinatorics, Geometry and Probability: A Tribute to Paul Erdős, edited by B. Bollobás and A. Thomason, Cambridge University Press, Cambridge, 1997, 1–10

work page 1997
[4]

Paul Erdős, Endre Makai, János Pach, Nearly equal distances in the plane,Combinatorics, Probability and Computing2(1993), 401–408

work page 1993
[5]

Gritzmann and B

Paul Erdős, Endre Makai, János Pach, Joel Spencer, Gaps in difference sets, and the graph of nearly equal distances, inApplied Geometry and Discrete Mathematics: The Victor Klee Festschrift, edited by P. Gritzmann and B. Sturmfels, DIMACS Series in Discrete Mathematics and Theoretical Computer Science4, American Mathematical Society, Providence, RI, 1991, 265–273

work page 1991
[6]

Nóra Frankl, Andrey Kupavskii, Nearlyk-Distance Sets,Discrete & Computational Geometry70(2023), 455–494

work page 2023
[7]

János Pach, Radoš Radoičić, Jan Vondrák, On the diameter of separated point sets with many nearly equal distances,European Journal of Combinatorics27(2006), 1321–1332

work page 2006
[8]

James Singer, A theorem in finite projective geometry and some applications to number theory,Transac- tions of the American Mathematical Society43(1938), 377–385

work page 1938

[1] [1]

Bloom,Erdős Problems,https://www.erdosproblems.com

Thomas F. Bloom,Erdős Problems,https://www.erdosproblems.com

work page

[2] [2]

Peter Brass, On the Erdős-diameter of sets,Discrete Mathematics150(1996), 415–419

work page 1996

[3] [3]

Bollobás and A

Paul Erdős, Some unsolved problems, inCombinatorics, Geometry and Probability: A Tribute to Paul Erdős, edited by B. Bollobás and A. Thomason, Cambridge University Press, Cambridge, 1997, 1–10

work page 1997

[4] [4]

Paul Erdős, Endre Makai, János Pach, Nearly equal distances in the plane,Combinatorics, Probability and Computing2(1993), 401–408

work page 1993

[5] [5]

Gritzmann and B

Paul Erdős, Endre Makai, János Pach, Joel Spencer, Gaps in difference sets, and the graph of nearly equal distances, inApplied Geometry and Discrete Mathematics: The Victor Klee Festschrift, edited by P. Gritzmann and B. Sturmfels, DIMACS Series in Discrete Mathematics and Theoretical Computer Science4, American Mathematical Society, Providence, RI, 1991, 265–273

work page 1991

[6] [6]

Nóra Frankl, Andrey Kupavskii, Nearlyk-Distance Sets,Discrete & Computational Geometry70(2023), 455–494

work page 2023

[7] [7]

János Pach, Radoš Radoičić, Jan Vondrák, On the diameter of separated point sets with many nearly equal distances,European Journal of Combinatorics27(2006), 1321–1332

work page 2006

[8] [8]

James Singer, A theorem in finite projective geometry and some applications to number theory,Transac- tions of the American Mathematical Society43(1938), 377–385

work page 1938