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/8c)n2(1/8 - c)n^2 edges then GG must contain either a K4K_4 or an independent set on at least n/lognn/\log n vertices?

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

615.lean

Retained formal statement2 of 4

The result of Fox, Loh, and Zhao [FLZ15] disproving the problem: if f(n)0f(n) \geq 0 satisfies f(n)=o(logn/loglogn)f(n) = o(\sqrt{\log n/\log\log n}), then for every ϵ>0\epsilon > 0 and all sufficiently large nn there is a K4K_4-free graph on nn vertices with independence number at most nef(n)ne^{-f(n)} and at least (1/8ϵ)n2(1/8 - \epsilon)n^2 edges; that is, rt(n;4,nef(n))(1/8o(1))n2\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2. Applied with f(n)=loglognf(n) = \log\log n, this disproves the headline problem, since nef(n)=n/logn=o(n)ne^{-f(n)} = n/\log n = o(n).

FormalConjectures/ErdosProblems/615.leanErdos615.erdos_615.variants.fox_loh_zhao7 linesExact file
∀ (f : ℕ → ℝ),  (∀ (n : ℕ), 0 ≤ f n) →    Filter.Tendsto (fun n => f n / √(Real.logn / Real.log (Real.logn))) 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.card
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page