Skip to content

Erdős problem 1082

Let AR2A\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

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1082.lean

Retained formal statement2 of 2

Let AR2A\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](https://www.erdosproblems.com/forum/thread/1082), 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.NonTrilinearAa, ∃ (_ : aA), 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.

Search problems.science

Find a Problem, Result, source, or page