Erdős Problem 99

References:

• erdosproblems.com/99
• [BeFo99] Bezdek, Andr'{a}s and Fodor, Ferenc, Minimal diameter of certain sets in the plane. J. Combin. Theory Ser. A (1999), 105-111.
• [Er94b] Erd\H{o}s, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.

def Erdos99.HasMinDist1 (A : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A set has minimum distance $1$ if all pairwise distances are at least $1$, and the minimum is achieved.

Equations

• Erdos99.HasMinDist1 A = ((∀ p ∈ A, ∀ q ∈ A, p ≠ q → dist p q ≥ 1) ∧ ∃ p ∈ A, ∃ q ∈ A, dist p q = 1)

def Erdos99.FormsEquilateralTriangle (p q r : EuclideanSpace ℝ (Fin 2)) : Prop

Three points form an equilateral triangle of side length 1.

Equations

• Erdos99.FormsEquilateralTriangle p q r = (dist p q = 1 ∧ dist q r = 1 ∧ dist p r = 1)

theorem Erdos99.erdos_99 : sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → HasMinDist1 A → IsMinOn (fun (B : Finset (EuclideanSpace ℝ (Fin 2))) => Metric.diam ↑B) {B : Finset (EuclideanSpace ℝ (Fin 2)) | B.card = n ∧ HasMinDist1 B} A → ∃ p ∈ A, ∃ q ∈ A, ∃ r ∈ A, FormsEquilateralTriangle p q r

For sufficiently large n, is it the case that any set of n points with minimum distance $1$ that minimizes diameter must contain an equilateral triangle of side length 1?