Skip to content

Erdős problem 22

Let ϵ>0\epsilon > 0 and let nn be sufficiently large depending on ϵ\epsilon. Is there a graph on nn vertices with at least n2/8n^2/8 many edges which contains no K4K_4, such that the largest independent set has size at most ϵn\epsilon n?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/22.lean

Formal Conjectures

FormalConjectures/ErdosProblems/22.leanErdos22.erdos_223 linesExact file
True  ∀ (ε : ℝ),    0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ ε * ↑n ∧ ↑n ^ 2 / 8 ≤ ↑G.edgeFinset.card
SolvedStatement only, no proof

Continue

Search problems.science

Find a Problem, Result, source, or page