Erdős problem 90 · problems.science

Conjectured upper bound on how many pairs among $n$ points in the plane can be exactly one unit apart.

Sources

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

9 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

90.lean

Retained formal statement8 of 8

This lemma confirms that the set of possible unit distance counts is bounded above, which ensures that taking the supremum (sSup) is a well-defined operation. The trivial upper bound is the total number of pairs of points, $\binom{n}{2}$ .

FormalConjectures/ErdosProblems/90.leanErdos90.unitDistanceCounts_BddAbove1 lineExact file

1∀ (n : ℕ), BddAbove (Erdos90.unitDistanceCounts n)

TestStatement only, no proof

Sources

Search problems.science