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 statement3 of 3

In [Er69b] Erdős conjectures this for f(m)=ϵmf(m)=\epsilon m for any fixed ϵ>0\epsilon>0. This follows from a result of Erdős, Hajnal, and Szemerédi [EHS82], as described by Sellke in the comments.

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