Combinatorics

Erdős problem 653

Let

x_1,\ldots,x_n\in \mathbb{R}^2

and let

R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}

, where the points are ordered such that

R(x_1)\leq \cdots \leq R(x_n).

Let

g(n)

be the maximum number of distinct values the

R(x_i)

can take. Is it true that

g(n) \geq (1-o(1))n

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«653»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos653.erdos_653" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∃ o,
    o =o[Filter.atTop] 1 ∧
      ∀ᶠ (n : ℕ) in Filter.atTop, (1 - o n) * ↑n ≤ ↑(EuclideanGeometry.maximalDistinctDistancesFrom n)

Original conjecture source: FormalConjectures/ErdosProblems/653.lean

Source type SHA-256: sha256:c6cf5fd197d3cabc9af95fa220fa6c8be2afaa41376cd5458cb0d9897f019b60
Task id: fc-v2-erdos653-erdos-653-8b5d740d81ae167d255963a2-formalized
Task commitment: sha256:a1715712f8407ff1bbe0c680c01c8852de5d8f1052254597517109074f359089

References

erdosproblems.com/653

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Erdős problem 653

Let

x_1,\ldots,x_n\in \mathbb{R}^2

and let

R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}

, where the points are ordered such that

R(x_1)\leq \cdots \leq R(x_n).

Let

g(n)

be the maximum number of distinct values the

R(x_i)

can take. Is it true that

g(n) \geq (1-o(1))n