Erdős problem 533 · problems.science

Let $\delta > 0$ . If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no $K_5$ and at least $\delta n^2$ edges, must $G$ contain a set of $\gg_\delta n$ vertices spanning no triangle?

Sources

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

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

533.lean

Retained formal statement4 of 6

The upper bound $\delta_3(5) \leq 1/12$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94]: for every $\epsilon > 0$ there is a $\delta > 0$ such that for all sufficiently large $n$ , every $K_5$ -free graph $G$ on $n$ vertices in which every triangle-free vertex set has at most $\delta n$ vertices has at most $(1/12 + \epsilon)n^2$ edges.

FormalConjectures/ErdosProblems/533.leanErdos533.erdos_533.variants.ehsss_upper9 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science