Erdős problem 755 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

755.lean

Retained formal statement1 of 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}$ .

FormalConjectures/ErdosProblems/755.leanErdos755.erdos_7552 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science