Skip to content

Erdős problem 655

Let x1,,xnR2x_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

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

655.lean

Retained formal statement2 of 2

Let x1,,xnR2x_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
Truec > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))),        X.card = n          Erdos655.IsValid X            EuclideanGeometry.InGeneralPositionX → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page