Erdős problem 22 · problems.science

Let $\epsilon > 0$ and let $n$ be sufficiently large depending on $\epsilon$ . Is there a graph on $n$ vertices with at least $n^2/8$ many edges which contains no $K_4$ , such that the largest independent set has size at most $\epsilon n$ ?

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

22.lean

Retained formal statement2 of 5

The construction of Bollobás and Erdős [BoEr76]: for every $\epsilon > 0$ and $\delta > 0$ , for all sufficiently large $n$ there is a $K_4$ -free graph on $n$ vertices with independence number at most $\delta n$ and at least $(1/8 - \epsilon)n^2$ edges. Together with erdos_22.variants.szemeredi_upper this shows that the Ramsey–Turán density of $K_4$ is $1/8$ .

FormalConjectures/ErdosProblems/22.leanErdos22.erdos_22.variants.bollobas_erdos_lower4 linesExact file

1∀ (ε δ : ℝ),2  0 < ε →3    0 < δ →4      ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ δ * ↑n ∧ (1 / 8 - ε) * ↑n ^ 2 ≤ ↑G.edgeFinset.card

SolvedStatement only, no proof

Sources

Search problems.science