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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/655.lean

Formal Conjectures

FormalConjectures/ErdosProblems/655.leanErdos655.erdos_6555 linesExact file
Falsec > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))),        X.card = nErdos655.IsValid X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page