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

The matching upper bound, due to Szemerédi [Sz72]: a $K_4$ -free graph on $n$ vertices whose independence number is sublinear in $n$ has at most $(1/8 + o(1))n^2$ edges. That is, for every $\epsilon > 0$ there is a $\delta > 0$ such that for all sufficiently large $n$ , every $K_4$ -free graph $G$ on $n$ vertices with $\alpha(G) \leq \delta n$ has at most $(1/8 + \epsilon)n^2$ edges.

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

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

SolvedStatement only, no proof

Sources

Search problems.science