Erdős problem 91
Suppose has and minimises the number of distinct distances between points in . Prove that for large there are at least two (and probably many) such which are non-similar.
Sources
FormalConjectures/ErdosProblems/
91.lean
Retained formal statement
Suppose has and minimises the number of distinct distances between points in . Prove that for large there are at least two (and probably many) such which are non-similar.
(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ TrueOpenStatement only, no proof