Erdős problem 579 · problems.science

Let $\delta > 0$ . If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no $K_{2,2,2}$ (the octahedron) and at least $\delta n^2$ edges, must $G$ contain an independent set of size $\gg_\delta n$ ?

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

579.lean

Retained formal statement2 of 3

The partial result of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]: the statement of erdos_579 holds whenever the edge-density coefficient exceeds $1/8$ . That is, for every $\delta > 1/8$ there is a $c > 0$ such that for all sufficiently large $n$ , every $K_{2,2,2}$ -free graph $G$ on $n$ vertices with at least $\delta n^2$ edges has an independent set of size at least $c n$ .

FormalConjectures/ErdosProblems/579.leanErdos579.erdos_579.variants.ehss_large_delta7 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science