Erdős problem 615
Does there exist some constant such that for all sufficiently large , if is a graph with vertices and at least edges then must contain either a or an independent set on at least vertices?
Sources
FormalConjectures/ErdosProblems/
615.lean
Retained formal statement
The result of Fox, Loh, and Zhao [FLZ15] disproving the problem: if satisfies , then for every and all sufficiently large there is a -free graph on vertices with independence number at most and at least edges; that is, . Applied with , this disproves the headline problem, since .
∀ (f : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ f n) → Filter.Tendsto (fun n => f n / √(Real.log ↑n / Real.log (Real.log ↑n))) Filter.atTop (nhds 0) → ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ ↑n * Real.exp (-f n) ∧ (1 / 8 - ε) * ↑n ^ 2 ≤ ↑G.edgeFinset.cardSolvedStatement only, no proof