Do diameter-minimising point sets with unit separation contain a unit equilateral triangle? (Erdős #99)
Statement
Let $A\subseteq\mathbb{R}^2$ be a set of $n$ points with minimum pairwise distance equal to $1$, chosen to minimise the diameter of $A$. If $n$ is sufficiently large, must there be three points of $A$ forming an equilateral triangle of side length $1$?
Acceptance. FULLY RESOLVES: a proof that for all sufficiently large $n$, every $n$-point diameter-minimising configuration with minimum distance $1$ contains a unit equilateral triangle (machine-checkable proof preferred, else complete written proof); OR a certified counterexample family — infinitely many $n$, each with a configuration proved optimal (rigorous optimality certificate, e.g. verified branch-and-bound) and proved to contain no unit equilateral triangle. Note a bare configuration is not enough: its diameter-minimality must be certified. ADVANCES: exact diameter-minimising configurations for values of $n$ beyond those resolved by Bezdek–Fodor as stated in the background, each with a reproducible optimality certificate and a determination of whether a unit equilateral triangle is present; or a proof of the structural conjecture that minimisers contain $(1-o(1))n$ points of a triangular lattice; or a proof of the statement for any explicit infinite subsequence of $n$. Deliver the proof file, or the optimisation code plus certificates and the configurations found.
Background
Posed by Erdős in [Er94b] and repeated in [Er95] and [Er97e]; listed as open on erdosproblems.com/99 (fetched 2026-07-13, status 'open', tagged 'geometry | distances'). Erdős put money on it asymmetrically: \$100 for a counterexample but only \$50 for a proof — he wrote in [Er94b] that he 'could not prove it but felt that it should not be hard', and was surprised when both B. H. Sendov and M. Simonovits doubted the conjecture. Context: by Thue's theorem on optimal circle packing, the minimal diameter of $n$ unit-separated points is achieved asymptotically by triangular-lattice points intersected with a disc, and Erdős believed any minimiser must have very large intersection with a triangular lattice — perhaps $(1-o(1))n$ points of it. The conjecture fails for small $n$: for $n=4$ the vertices of a unit square minimise the diameter and contain no unit equilateral triangle. The structure of these diameter-minimising 'spreading points' configurations for small $n$ was worked out by Bezdek and Fodor [BeFo99]. A companion question on the maximum number of unit distances in such minimisers is Erdős #103 (erdosproblems.com/103). The statement is formalised in Lean in DeepMind's formal-conjectures repository. The attacker's tools: rigorous global optimisation (interval-arithmetic branch-and-bound over configurations, in the style of certified circle-packing results) to determine exact minimisers for new values of $n$ and test them for unit equilateral triangles, plus lattice-rigidity arguments for the asymptotic regime.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #99 (T. F. Bloom) | website |
| REF-02 | Formalised Lean statement of Erdős #99 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.