Erdős problem 91

Suppose $A\subset \mathbb{R}^2$ has $\lvert A\rvert=n$ and minimises the number of distinct distances between points in $A$ . Prove that for large $n$ there are at least two (and probably many) such $A$ which are non-similar.

Sources

The source's own material, retained exactly.

14 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

91.lean

Retained formal statement1 of 14

Suppose $A\subset \mathbb{R}^2$ has $\lvert A\rvert=n$ and minimises the number of distinct distances between points in $A$ . Prove that for large $n$ there are at least two (and probably many) such $A$ which are non-similar.

FormalConjectures/ErdosProblems/91.leanErdos91.erdos_911 lineExact file

1(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ True

OpenStatement only, no proof