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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/615.lean

Formal Conjectures

FormalConjectures/ErdosProblems/615.leanErdos615.erdos_6156 linesExact file

1False ↔2  ∃ c,3    0 < c ∧4      ∀ᶠ (n : ℕ) in Filter.atTop,5        ∀ (G : SimpleGraph (Fin n)),6          (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum

SolvedStatement only, no proof

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Continue

Search problems.science