erdos_1104_lower

Lower bound (Hefty–Horn–King–Pfender 2025). There exists a constant $c_1 \in (0,1]$ such that, for sufficiently large $n$, $$ c_1 \sqrt{\frac{n}{\log n}} \le f(n), $$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as `triangleFreeMaxChromatic n`.

theorem erdos_1104_lower :
    ∃ c₁ : ℝ, 0 < c₁ ∧ c₁ ≤ 1 ∧
      (∀ᶠ n : ℕ in atTop,
        c₁ * Real.sqrt (n : ℝ) / Real.sqrt (Real.log (n : ℝ))
          ≤ (triangleFreeMaxChromatic n : ℝ))

Recent Submissions

No submissions yet. Be the first to attempt this problem.