Independent sets in graphs of infinite chromatic number

DefinitionErdős Problem 750#✓fully proved

The statement that the following three assertions all hold. (i) For every function \(f : \mathbb{N} \to \mathbb{R}_{\ge 0}\) with \(f(m) \to \infty\) as \(m \to \infty\) there is a simple graph \(G\) with infinite chromatic number such that for every \(m > 0\), every set \(S\) of exactly \(m\) vertices of \(G\) contains an independent set \(I\) of \(G\) with \(|I| \ge m/2 - f(m)\). (ii) For every real \(\varepsilon > 0\) there is a simple graph \(G\) with infinite chromatic number such that for every \(m > 0\), every set of exactly \(m\) vertices of \(G\) contains an independent set of \(G\) with at least \(m/2 - \varepsilon m\) elements. (iii) For every real \(c > 1/4\) there is a simple graph \(G\) with infinite chromatic number such that for every \(m > 0\), every set of exactly \(m\) vertices of \(G\) contains an independent set of \(G\) with at least \(m/2 - cm\) elements.

def conjecture : Prop :=
  (∀ f : ℕ → ℝ≥0, atTop.Tendsto f atTop →
    ∃ (V : Type) (G : SimpleGraph V),
      G.chromaticNumber = ⊤ ∧
      ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
        ∃ I ⊆ S, G.IsIndepSet I ∧ (m : ℝ) / 2 - f m ≤ I.ncard) ∧
  (∀ ε : ℝ≥0, 0 < ε →
    ∃ (V : Type) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
      ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
        ∃ I ⊆ S, G.IsIndepSet I ∧ (m : ℝ) / 2 - ε * m ≤ I.ncard) ∧
  (∀ c : ℝ≥0, 1 / 4 < c →
    ∃ (V : Type) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
      ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
        ∃ I ⊆ S, G.IsIndepSet I ∧ (m : ℝ) / 2 - c * m ≤ I.ncard)

Used by 1

Used byErdős Problem 750 is true

TheoremErdős Problem 750 is true#●ready to prove

The following three statements hold. (i) For every function \(f : \mathbb{N} \to \mathbb{R}_{\ge 0}\) with \(f(m) \to \infty\) as \(m \to \infty\) there is a simple graph \(G\) with infinite chromatic number such that for every \(m > 0\), every set \(S\) of exactly \(m\) vertices of \(G\) contains an independent set \(I\) of \(G\) with \(|I| \ge m/2 - f(m)\). (ii) For every real \(\varepsilon > 0\) there is a simple graph \(G\) with infinite chromatic number such that for every \(m > 0\), every set of exactly \(m\) vertices of \(G\) contains an independent set of \(G\) with at least \(m/2 - \varepsilon m\) elements. (iii) For every real \(c > 1/4\) there is a simple graph \(G\) with infinite chromatic number such that for every \(m > 0\), every set of exactly \(m\) vertices of \(G\) contains an independent set of \(G\) with at least \(m/2 - cm\) elements.

public theorem_wanted conjecture_holds : conjecture

Sources

• plby/lean-proofs, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos750.lean#L41.

Uses 1

Statement usesErdős Problem 750

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.