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

A sanity check for erdos_22.variants.szemeredi_upper: the empty graph is $K_4$ -free and trivially satisfies the upper bound $(1/8 + \epsilon)n^2$ on the number of edges.

FormalConjectures/ErdosProblems/22.leanErdos22.erdos_22.variants.test_bot1 lineExact file

1∀ (n : ℕ) (ε : ℝ), 0 < ε → ⊥.CliqueFree 4 ∧ ↑⊥.edgeFinset.card ≤ (1 / 8 + ε) * ↑n ^ 2

TestStatement only, no proof

Sources

Search problems.science