Skip to content

Erdős problem 750

Start work

Let f(m)f(m) be some function such that f(m)→∞f(m)\to \infty as m→∞m\to \infty. Does there exist a graph GG of infinite chromatic number such that every subgraph on mm vertices contains an independent set of size at least m2−f(m)\frac{m}{2}-f(m)?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

750.lean

Retained formal statement2 of 3

In [ErHa67b] Erdős and Hajnal prove this for f(m)≥cmf(m)\geq cm for all c>1/4c>1/4.

FormalConjectures/ErdosProblems/750.leanErdos750.erdos_750.variants.c_gt_quarter5 linesExact file
True ↔  ∀ c > 1 / 4,    ∃ V G,      G.chromaticNumber = ⊤ ∧        ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m → ∃ I ⊆ S, G.IsIndepSet I ∧ ↑m / 2 - c * ↑m ≤ ↑I.ncard
SolvedStatement only, no proof