Erdős Problem 1104

Reference: https://www.erdosproblems.com/1104

noncomputable def Erdos1104.triangleFreeMaxChromatic (n : ℕ) : ℕ

Maximum chromatic number of a triangle-free graph on n vertices.

Equations

• Erdos1104.triangleFreeMaxChromatic n = sSup {χ : ℕ | ∃ (G : SimpleGraph (Fin n)), G.CliqueFree 3 ∧ G.chromaticNumber = ↑χ}

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

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 Erdos1104.erdos_1104_upper : ∃ (c₂ : ℝ), 2 ≤ c₂ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(triangleFreeMaxChromatic n) ≤ c₂ * √↑n / √(Real.log ↑n)

Upper bound (Davies–Illingworth 2022). There exists a constant $c_2 \ge 2$ such that, for sufficiently large $n$, $$ f(n) \le c_2 \sqrt{\frac{n}{\log n}}, $$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as triangleFreeMaxChromatic n.