Reed's omega, delta, and chi conjecture

References:

• B. Reed, ω Δ and χ, J. Graph Theory 27 (1998) 177-212.
• openproblemgarden
• mathoverflow/37923 asked by user Andrew D. King

theorem ReedOmegaDeltaChi.reed_omega_delta_chi_conjecture {V : Type} (G : SimpleGraph V) : have χ := G.chromaticNumber; have ω := G.ecliqueNum; have Δ := G.emaxDegree; 2 * χ ≤ ω + Δ + 2

For a graph $G$, we define $\Delta(G)$ to be the maximum degree, $\omega(G)$ to be the size of the largest clique subgraph, and $\chi(G)$ to be the chromatic number. Reed's omega, delta, and chi conjecture states that $$\chi(G) \leq \lceil \frac{1}{2}(\omega(G) + \Delta(G) + 1) \rceil.$$

theorem ReedOmegaDeltaChi.reed_omega_delta_chi_conjecture_for_finite_graphs {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : have χ := G.chromaticNumber; have ω := G.cliqueNum; have Δ := G.maxDegree; 2 * χ ≤ ↑ω + ↑Δ + 2

For a finite graph $G$, we define $\Delta(G)$ to be the maximum degree, $\omega(G)$ to be the size of the largest clique subgraph, and $\chi(G)$ to be the chromatic number. Reed's omega, delta, and chi conjecture states that $$\chi(G) \leq \lceil \frac{1}{2}(\omega(G) + \Delta(G) + 1) \rceil.$$

theorem ReedOmegaDeltaChi.reed_conjecture_Δ_6_ω_2 {V : Type} (G : SimpleGraph V) : G.emaxDegree = 6 ∧ G.cliqueNum = 2 → G.chromaticNumber ≤ 5

The simplest open case is when $\Delta(G) = 6$ and $\omega(G) = 2$.