Equilateral triangles in planar point sets

DefinitionEquilateral triangle with given side#✓fully proved

For a real number \(s\), a finite set \(T\) of points in the Euclidean space \(\mathbb{R}^d\) is an equilateral triangle of side \(s\) when \(T\) has exactly three elements and any two distinct points of \(T\) are at distance \(s\).

def IsEquilateralTriangle {d : ℕ} (side : ℝ)
    (T : Finset (EuclideanSpace ℝ (Fin d))) : Prop :=
  T.card = 3 ∧ ∀ p ∈ T, ∀ q ∈ T, p ≠ q → dist p q = side

Used by 2

Used byEquilateral triangle of any size · Unit equilateral triangle

DefinitionUnit equilateral triangle#✓fully proved

A finite set \(T\) of points in the Euclidean space \(\mathbb{R}^d\) is a unit equilateral triangle when it is an equilateral triangle of side \(1\): \(T\) has exactly three elements and any two distinct points of \(T\) are at distance \(1\).

def IsUnitEquilateralTriangle {d : ℕ}
    (T : Finset (EuclideanSpace ℝ (Fin d))) : Prop :=
  IsEquilateralTriangle 1 T

Uses 1 · Used by 1

Statement usesEquilateral triangle with given side

Used byNumber of unit equilateral triangles in a point set

DefinitionEquilateral triangle of any size#✓fully proved

A finite set \(T\) of points in the Euclidean space \(\mathbb{R}^d\) is an equilateral triangle of any size when there is a real number \(s > 0\) such that \(T\) is an equilateral triangle of side \(s\): \(T\) has exactly three elements and any two distinct points of \(T\) are at distance \(s\).

def IsAnySizeEquilateralTriangle {d : ℕ}
    (T : Finset (EuclideanSpace ℝ (Fin d))) : Prop :=
  ∃ side : ℝ, 0 < side ∧ IsEquilateralTriangle side T

Uses 1 · Used by 1

Statement usesEquilateral triangle with given side

Used byNumber of equilateral triangles in a point set

DefinitionNumber of unit equilateral triangles in a point set#✓fully proved

For a finite set \(P\) of points in the Euclidean space \(\mathbb{R}^d\), this is the number of three-element subsets of \(P\) that are unit equilateral triangles, that is, whose three points are pairwise at distance \(1\).

noncomputable def unitEquilateralTriangleCount (d : ℕ)
    (P : Finset (EuclideanSpace ℝ (Fin d))) : ℕ :=
  open scoped Classical in
  ((P.powersetCard 3).filter fun T => IsUnitEquilateralTriangle T).card

Uses 1 · Used by 1

Statement usesUnit equilateral triangle

Used byMaximum number of unit equilateral triangles

DefinitionNumber of equilateral triangles in a point set#✓fully proved

For a finite set \(P\) of points in the Euclidean space \(\mathbb{R}^d\), this is the number of three-element subsets of \(P\) that are equilateral triangles of some positive side length \(s\), that is, whose three points are pairwise at distance \(s\).

noncomputable def anySizeEquilateralTriangleCount (d : ℕ)
    (P : Finset (EuclideanSpace ℝ (Fin d))) : ℕ :=
  open scoped Classical in
  ((P.powersetCard 3).filter fun T => IsAnySizeEquilateralTriangle T).card

Uses 1 · Used by 1

Statement usesEquilateral triangle of any size

Used byMaximum number of equilateral triangles

DefinitionMaximum number of unit equilateral triangles#✓fully proved

For natural numbers \(d\) and \(n\), \(T_1(d, n)\) is the supremum in \(\mathbb{N}\), over all sets \(P\) of exactly \(n\) points in the Euclidean space \(\mathbb{R}^d\), of the number of unit equilateral triangles spanned by \(P\) (the three-element subsets of \(P\) whose points are pairwise at distance \(1\)). When such sets exist this is the largest such number; when none exist (only for \(d = 0\) and \(n \ge 2\)) it is \(0\).

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

Uses 1 · Used by 1

Statement usesNumber of unit equilateral triangles in a point set

Used byStatement of Erdős Problem 755

DefinitionMaximum number of equilateral triangles#✓fully proved

For natural numbers \(d\) and \(n\), \(T(d, n)\) is the supremum in \(\mathbb{N}\), over all sets \(P\) of exactly \(n\) points in the Euclidean space \(\mathbb{R}^d\), of the number of equilateral triangles of positive side length spanned by \(P\) (the three-element subsets of \(P\) whose points are pairwise at the same positive distance). When such sets exist this is the largest such number; when none exist (only for \(d = 0\) and \(n \ge 2\)) it is \(0\).

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

Uses 1 · Used by 1

Statement usesNumber of equilateral triangles in a point set

Used byStatement of Erdős Problem 755

DefinitionStatement of Erdős Problem 755#✓fully proved

Let \(T_1(n)\) be the largest number of unit equilateral triangles spanned by a set of \(n\) points in \(\mathbb{R}^6\), and let \(T(n)\) be the largest number of equilateral triangles of positive side length spanned by a set of \(n\) points in \(\mathbb{R}^6\); a triangle spanned by a set is a three-element subset of it whose points are pairwise at the same distance. The statement asserts both of the following: there is a function \(o : \mathbb{N} \to \mathbb{R}\) with \(o(n) \to 0\) as \(n \to \infty\) such that \(T_1(n) \le (1/27 + o(n))\, n^3\) for all sufficiently large \(n\); and \(T(n)\) is asymptotically equivalent to \(n^3/27\) as \(n \to \infty\).

def conjecture : Prop :=
  (∃ o : ℕ → ℝ,
    o =o[atTop] (fun _ : ℕ => (1 : ℝ)) ∧
      ∀ᶠ n in atTop,
        (TUnit 6 n : ℝ) ≤ ((1 / 27 : ℝ) + o n) * (n : ℝ) ^ 3) ∧
  ((fun n : ℕ => (TAnySize 6 n : ℝ)) ~[atTop]
    (fun n : ℕ => (1 / 27 : ℝ) * (n : ℝ) ^ 3))

Uses 2 · Used by 1

Statement usesMaximum number of equilateral triangles · Maximum number of unit equilateral triangles

Used byErdős Problem 755 holds (Clemen–Dumitrescu–Liu)

TheoremErdős Problem 755 holds (Clemen–Dumitrescu–Liu)#●ready to prove

Let \(T_1(n)\) be the largest number of unit equilateral triangles spanned by a set of \(n\) points in \(\mathbb{R}^6\), and let \(T(n)\) be the largest number of equilateral triangles of positive side length spanned by a set of \(n\) points in \(\mathbb{R}^6\); a triangle spanned by a set is a three-element subset of it whose points are pairwise at the same distance. Then there is a function \(o : \mathbb{N} \to \mathbb{R}\) with \(o(n) \to 0\) as \(n \to \infty\) such that \(T_1(n) \le (1/27 + o(n))\, n^3\) for all sufficiently large \(n\), and \(T(n)\) is asymptotically equivalent to \(n^3/27\) as \(n \to \infty\).

public theorem_wanted conjecture_holds : conjecture

Sources

• Felix Christian Clemen, Adrian Dumitrescu, and Dingyuan Liu, The number of regular simplices in higher dimensions, arXiv:2507.19841 (2025), https://arxiv.org/abs/2507.19841. Resolved true: Resolved externally by Clemen, Dumitrescu, and Liu. This repository records the statement, not an internal proof; a separate pinned Lean proof is cited in the registry.

Uses 1

Statement usesStatement of Erdős Problem 755

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.