Skip to content

Erdős problem 653

Let x1,…,xn∈R2x_1,\ldots,x_n\in \mathbb{R}^2 and let R(xi)=#{∣xj−xi∣:j≠i}R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}, where the points are ordered such that R(x1)≤⋯≤R(xn).R(x_1)\leq \cdots \leq R(x_n). Let g(n)g(n) be the maximum number of distinct values the R(xi)R(x_i) can take. Is it true that g(n)≥(1−o(1))ng(n) \geq (1-o(1))n?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

653.lean

Retained formal statement1 of 1

Let x1,…,xn∈R2x_1,\ldots,x_n\in \mathbb{R}^2 and let R(xi)=#{∣xj−xi∣:j≠i}R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}, where the points are ordered such that R(x1)≤⋯≤R(xn).R(x_1)\leq \cdots \leq R(x_n). Let g(n)g(n) be the maximum number of distinct values the R(xi)R(x_i) can take. Is it true that g(n)≥(1−o(1))ng(n) \geq (1-o(1))n?

FormalConjectures/ErdosProblems/653.leanErdos653.erdos_6534 linesExact file
True ↔  ∃ o,    o =o[Filter.atTop] 1 ∧      ∀ᶠ (n : ℕ) in Filter.atTop, (1 - o n) * ↑n ≤ ↑(EuclideanGeometry.maximalDistinctDistancesFrom n)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page