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 statement4 of 4

A sanity check for erdos_615: the empty graph on $n \geq 3$ vertices contains an independent set on at least $n/\log n$ vertices (namely the whole vertex set), so it satisfies the conclusion of the implication in the problem statement.

FormalConjectures/ErdosProblems/615.leanErdos615.erdos_615.variants.test_bot1 lineExact file

1∀ (n : ℕ), 3 ≤ n → ↑n / Real.log ↑n ≤ ↑⊥.indepNum

TestStatement only, no proof

Sources

Search problems.science