Skip to content

Erdős problem 615

Does there exist some constant c>0c > 0 such that for all sufficiently large nn, if GG is a graph with nn vertices and at least (1/8−c)n2(1/8 - c)n^2 edges then GG must contain either a K4K_4 or an independent set on at least n/log⁡nn/\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 statement1 of 4

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

The answer is no, as shown by Fox, Loh, and Zhao [FLZ15].

FormalConjectures/ErdosProblems/615.leanErdos615.erdos_6156 linesExact file
False ↔  ∃ c,    0 < c ∧      ∀ᶠ (n : ℕ) in Filter.atTop,        ∀ (G : SimpleGraph (Fin n)),          (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page