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?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1082.lean

Retained formal statement2 of 2

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?

This question has been answered negatively by Xichuan in the comments, who gave a set of 4242 points in R2\mathbb{R}^2, with no three on a line, such that each point determines only 2020 distinct distances.

A smaller counterexample has been formalised here: it comprised of 88 points, where each point only determines 33 distances.

This counterexample has originally been found by Heiko Harborth.

FormalConjectures/ErdosProblems/1082.leanErdos1082.erdos_1082.parts.ii5 linesExact file
False ↔  ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),    A.Nonempty →      EuclideanGeometry.NonTrilinear ↑A →        ∃ a, ∃ (_ : a ∈ A), A.card / 2 ≤ EuclideanGeometry.distinctDistancesFrom A a - 1
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.