Skip to content

Erdős problem 655

Let x1,…,xn∈R2x_1,\ldots,x_n\in \mathbb{R}^2 be such that no circle whose centre is one of the xix_i contains three other points. Are there at least (1+c)n2(1+c)\frac{n}{2} distinct distances determined between the xix_i, for some constant c>0c>0 and all nn sufficiently large?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

655.lean

Retained formal statement2 of 2

Let x1,…,xn∈R2x_1,\ldots,x_n\in \mathbb{R}^2 be such that no circle whose centre is one of the xix_i contains three other points. Are there at least(1+c)n2(1+c)\frac{n}{2} distinct distances determined between the xix_i, for some constant c>0c>0 and all nn sufficiently large?

In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position (e.g. no three on a line and no four on a circle) was intended.

FormalConjectures/ErdosProblems/655.leanErdos655.erdos_655.variants.general_position7 linesExact file
True ↔  ∃ c > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))),        X.card = n →          Erdos655.IsValid X →            EuclideanGeometry.InGeneralPosition ↑X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)
OpenStatement only, no proof