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

FormalConjectures/ErdosProblems/

755.lean

Retained formal statement3 of 3

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

FormalConjectures/ErdosProblems/755.leanErdos755.erdos_755.variants.any_size_cdl1 lineExact file

1Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos755.TAnySize 6 n)) fun n => 1 / 27 * ↑n ^ 3

SolvedStatement only, no proof