Skip to content

Erdős problem 1082

Let A⊂R2A\subset \mathbb{R}^2 be a set of nn points with no three on a line. Must there exist a single point from which there are at least ⌊n/2⌋\lfloor n/2\rfloor distinct distances?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1082.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1082.leanErdos1082.erdos_1082.parts.i3 linesExact file
True ↔  ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),    EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A
OpenStatement only, no proof

Reported activity

Reported by these sources. Not reviewed here.

  • AI alongside literature

    Erdős AI contributions wiki · 14 Feb, 2026

    Machine
    DeepMind prover agent
    Open the source record

Continue