Erdős problem 615 · problems.science

Does there exist some constant $c > 0$ such that for all sufficiently large $n$ , if $G$ is a graph with $n$ vertices and at least $(1/8 - c)n^2$ edges then $G$ must contain either a $K_4$ or an independent set on at least $n/\log n$ vertices?

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

615.lean

Retained formal statement3 of 4

The complementary result of Sudakov [Su03]: if $f(n)/\sqrt{\log n} \to \infty$ then $\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)$ ; that is, for every $\epsilon > 0$ and all sufficiently large $n$ , every $K_4$ -free graph on $n$ vertices with independence number at most $ne^{-f(n)}$ has at most $\epsilon n^2$ edges.

FormalConjectures/ErdosProblems/615.leanErdos615.erdos_615.variants.sudakov7 linesExact file

1∀ (f : ℕ → ℝ),2  Filter.Tendsto (fun n => f n / √(Real.log ↑n)) Filter.atTop Filter.atTop →3    ∀ (ε : ℝ),4      0 < ε →5        ∀ᶠ (n : ℕ) in Filter.atTop,6          ∀ (G : SimpleGraph (Fin n)),7            G.CliqueFree 4 → ↑G.indepNum ≤ ↑n * Real.exp (-f n) → ↑G.edgeFinset.card ≤ ε * ↑n ^ 2

SolvedStatement only, no proof

Sources

Search problems.science