Skip to content

Erdős problem 22

Let ϵ>0\epsilon > 0 and let nn be sufficiently large depending on ϵ\epsilon. Is there a graph on nn vertices with at least n2/8n^2/8 many edges which contains no K4K_4, such that the largest independent set has size at most ϵn\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 statement1 of 5

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

This is true, as proved by Fox, Loh, and Zhao [FLZ15].

FormalConjectures/ErdosProblems/22.leanErdos22.erdos_223 linesExact file
True ↔  ∀ (ε : ℝ),    0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ ε * ↑n ∧ ↑n ^ 2 / 8 ≤ ↑G.edgeFinset.card
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page