Integer-distance point sets in general position: does every n admit one? (Erdős #213)
Statement
Let $n\geq 4$. Are there $n$ points in $\mathbb{R}^2$, no three on a line and no four on a circle, such that all pairwise distances are integers? (Sets avoiding three collinear and four concyclic points are said to be in general position; integer-distance sets in general position are known in the literature as integral point sets in general position.)
Acceptance. FULLY RESOLVES: determine for which $n\geq 4$ such configurations exist — either a construction scheme, with complete proof, producing a general-position integer-distance set of every size $n$; or an UNCONDITIONAL proof of an absolute upper bound $n_{\max}$ together with existence settled for each $n\le n_{\max}$ (a bound conditional on Bombieri–Lang does not qualify — that is already known, per Ascher–Braune–Turchet as stated in the background). Machine-checkable (Lean/Coq) proof preferred, else a complete written proof. ADVANCES: (a) an explicit example with $n=8$ (or any $n$ strictly beyond the $n=7$ record stated in the background): exact integer or rational coordinates plus a machine-verifiable certificate that all pairwise distances are integers, no three points are collinear, and no four are concyclic — this milestone coincides with the venue's integral-point-set search problem, and settles $n=8$ but not the full question; (b) an exhaustive, reproducible search certificate that no 8-point example exists up to an explicitly stated diameter bound strictly extending previously published searches (state and cite the prior record beaten), with code; (c) an unconditional size bound quantitatively stronger than the polylogarithmic sparsity bound of Greenfeld–Iliopoulou–Peluse stated in the background; (d) an explicit value or weaker hypothesis for the conditional uniform bound. Deliver the witness coordinates plus verification script, or the search code with its exhaustiveness certificate and attained bound, or the proof file.
Background
Posed by Erdős in [Er75f, p.106] and repeated in [Er83c] and [Er87b, p.172]; listed as open on erdosproblems.com/213 (fetched 2026-07-13, status 'open', tagged 'geometry | distances'). The infinite version is closed: Anning and Erdős [AnEr45] proved there is no infinite such set (the classical Erdős–Anning theorem — an infinite plane set with all pairwise distances integers must be collinear), so the question is how large a finite general-position example can be, and whether every size $n$ is achievable. Construction record: Harborth found an example with $n=5$; the best construction to date, due to Kreisel and Kurz [KK08], has $n=7$ (a 7-point integral point set in general position of diameter 22270). No 8-point example is known despite substantial computer searches — the concrete $n=8$ hunt is already on this venue as the neighbouring problem 'Integral point sets in general position: find an 8-point set / improve minimum diameters'; the present problem carries the full for-every-$n$ question. On the impossibility side, Ascher, Braune and Turchet [ABT20] showed that, conditional on the Bombieri–Lang conjecture, there is a uniform upper bound on the size of such a set. Unconditionally, Greenfeld, Iliopoulou and Peluse [GIP24] proved such sets must be extremely sparse: if $S\subseteq[-N,N]^2$ has no three points on a line, no four on a circle, and all pairwise distances integers, then $$\lvert S\rvert\ll(\log N)^{O(1)}.$$ A related problem is Erdős #130 (erdosproblems.com/130). The statement is formalised in Lean in DeepMind's formal-conjectures repository. The attacker's tools: large-scale exact search for an 8-point witness (enumeration of integral point sets by diameter and characteristic in the style of Kurz's searches, or constraint/SAT solving over exact arithmetic), exhaustive-search certificates ruling out small-diameter 8-point sets, and arithmetic geometry for unconditional size bounds.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #213 (T. F. Bloom) | website |
| REF-02 | R. Greenfeld, M. Iliopoulou, S. Peluse — On integer distance sets [GIP24] | arxiv |
| REF-03 | Formalised Lean statement of Erdős #213 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.