Erdős Problem 755

References:

• erdosproblems.com/755
• [ErPu75] Erdős, Paul and Purdy, George, Some extremal problems in geometry. III. (1975), 291--308.
• [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261--269.
• [CDL25b] Clemen, Felix Christian, Dumitrescu, Adrian, and Liu, Dingyuan, The number of regular simplices in higher dimensions. arXiv:2507.19841 (2025).

def Erdos755.IsEquilateralTriangle {d : ℕ} (side : ℝ) (T : Finset (EuclideanSpace ℝ (Fin d))) : Prop

A three-point set whose pairwise distances are all equal to side.

Equations

• Erdos755.IsEquilateralTriangle side T = (T.card = 3 ∧ ∀ p ∈ T, ∀ q ∈ T, p ≠ q → dist p q = side)

def Erdos755.IsUnitEquilateralTriangle {d : ℕ} (T : Finset (EuclideanSpace ℝ (Fin d))) : Prop

A unit equilateral triangle in Euclidean d-space.

Equations

• Erdos755.IsUnitEquilateralTriangle T = Erdos755.IsEquilateralTriangle 1 T

def Erdos755.IsAnySizeEquilateralTriangle {d : ℕ} (T : Finset (EuclideanSpace ℝ (Fin d))) : Prop

An equilateral triangle of any positive side length in Euclidean d-space.

Equations

• Erdos755.IsAnySizeEquilateralTriangle T = ∃ (side : ℝ), 0 < side ∧ Erdos755.IsEquilateralTriangle side T

noncomputable def Erdos755.unitEquilateralTriangleCount (d : ℕ) (P : Finset (EuclideanSpace ℝ (Fin d))) : ℕ

Number of unit equilateral triangles spanned by a finite point set.

Equations

• Erdos755.unitEquilateralTriangleCount d P = {T ∈ Finset.powersetCard 3 P | Erdos755.IsUnitEquilateralTriangle T}.card

noncomputable def Erdos755.anySizeEquilateralTriangleCount (d : ℕ) (P : Finset (EuclideanSpace ℝ (Fin d))) : ℕ

Number of equilateral triangles of any positive side length spanned by a finite point set.

Equations

• Erdos755.anySizeEquilateralTriangleCount d P = {T ∈ Finset.powersetCard 3 P | Erdos755.IsAnySizeEquilateralTriangle T}.card

noncomputable def Erdos755.TUnit (d n : ℕ) : ℕ

Maximum number of unit equilateral triangles spanned by $n$ points in $\mathbb{R}^d$.

Equations

• Erdos755.TUnit d n = sSup {m : ℕ | ∃ (P : Finset (EuclideanSpace ℝ (Fin d))), P.card = n ∧ Erdos755.unitEquilateralTriangleCount d P = m}

noncomputable def Erdos755.TAnySize (d n : ℕ) : ℕ

Maximum number of equilateral triangles of any size spanned by $n$ points in $\mathbb{R}^d$.

Equations

• Erdos755.TAnySize d n = sSup {m : ℕ | ∃ (P : Finset (EuclideanSpace ℝ (Fin d))), P.card = n ∧ Erdos755.anySizeEquilateralTriangleCount d P = m}

theorem Erdos755.erdos_755.test_dim_one : unitEquilateralTriangleCount 1 ∅ = 0

theorem Erdos755.erdos_755 : True ↔ ∃ (o : ℕ → ℝ), (o =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(TUnit 6 n) ≤ (1 / 27 + o n) * ↑n ^ 3

Erdős asked whether every $n$-point set in $\mathbb{R}^6$ spans at most $(1/27 + o(1)) n^3$ unit equilateral triangles.

Clemen, Dumitrescu, and Liu [CDL25b] proved the stronger any-size statement $T_6(n) = (1/27 + o(1)) n^3$. The unit-triangle upper bound follows as a corollary, since unit equilateral triangles are a subset of equilateral triangles of any positive side length: $T_\mathrm{unit} \leq T_\mathrm{anysize}$.

theorem Erdos755.erdos_755.variants.any_size_cdl : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(TAnySize 6 n)) fun (n : ℕ) => 1 / 27 * ↑n ^ 3

Clemen, Dumitrescu, and Liu [CDL25b] proved the stronger version where equilateral triangles of all positive side lengths are counted.