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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/755.lean

Formal Conjectures

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