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 statement3 of 5

The quantitative strengthening proved by Fox, Loh, and Zhao [FLZ15]: there is a constant $C > 0$ such that for all sufficiently large $n$ there exists a $K_4$ -free graph on $n$ vertices with at least $n^2/8$ edges whose largest independent set has size at most $C \cdot \frac{(\log\log n)^{3/2}}{(\log n)^{1/2}} \cdot n.$

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

1∃ C,2  0 < C ∧3    ∀ᶠ (n : ℕ) in Filter.atTop,4      ∃ G,5        G.CliqueFree 4 ∧6          ↑G.indepNum ≤ C * Real.log (Real.log ↑n) ^ (3 / 2) / Real.log ↑n ^ (1 / 2) * ↑n ∧7            ↑n ^ 2 / 8 ≤ ↑G.edgeFinset.card

SolvedStatement only, no proof

Sources

Search problems.science