Skip to content

Erdős problem 579

Let δ>0\delta > 0. If nn is sufficiently large and GG is a graph on nn vertices with no K2,2,2K_{2,2,2} (the octahedron) and at least δn2\delta n^2 edges, must GG contain an independent set of size δn\gg_\delta n?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/579.lean

Formal Conjectures

FormalConjectures/ErdosProblems/579.leanErdos579.erdos_5798 linesExact file
True  ∀ (δ : ℝ),    0 < δ →c,        0 < c          ∀ᶠ (n : ℕ) in Filter.atTop,            ∀ (G : SimpleGraph (Fin n)),              Erdos579.octahedron.Free G → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.cardc * ↑n ≤ ↑G.indepNum
OpenStatement only, no proof

Continue

Search problems.science

Find a Problem, Result, source, or page