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?

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
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

Continue