Erdős Problem #660

The question

Let $x_1,\dots ,x_n\in {\mathbb{R}}^3$ be the vertices of a convex polyhedron. Are there at least $$(1-o(1))\frac{n}{2}$$ many distinct distances between the $x_i$?

The $(1-o(1))\frac{n}{2}$ lower bound is formalised as: for every $\epsilon >0$, every set of $n$ vertices of a convex polyhedron with $n$ sufficiently large determines at least $(1-\epsilon )\frac{n}{2}$ distinct distances.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«660». answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem erdos_660 :
    answer(sorry) ↔
      ∀ ε : ℝ, 0 < ε → ∀ᶠ n in Filter.atTop, ∀ P : Finset ℝ³,
        P.card = n → IsPolyhedronVertices P →
        (1 - ε) * ((n : ℝ) / 2) ≤ (distinctDistances P : ℝ)

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/660. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Variants

• erdos_660.variants.Er75f — In [Er75f] Erdős claims that Altman proved that the vertices determine ≫ n many distinct distances, but gives no reference.

References

• erdosproblems.com/660
• [Er97e] Erdős, Paul, Some of my favorite problems and results, The mathematics of Paul Erdős, I (1997), 47–67.
• [Al63] Altman, E., On a problem of P. Erdős, Amer. Math. Monthly (1963), 148–157.
• [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry, Ann. Mat. Pura Appl. (4) (1975), 99–108.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.