Part 1 of 2

• Centered colorings
• Chromatic number of (0,2)-graphs
• Chromatic number of wheel-free graphs
• Color-critical graphs
• Cycle lengths in graphs of large chromatic number
• Degeneracy and greedy coloring
• Edge coloring
• Four color theorem
• Fractional coloring
• Hajnal–Szemerédi theorem
• Independent sets in graphs of infinite chromatic number
• Kneser graphs
• List coloring
• Odd distance graph
• Perfect graphs
• Petersen coloring conjecture
• Subgraphs of large cochromatic number
• Triangle-free subgraphs of large chromatic number

TheoremBrooks' theorem#✓fully proved

Let \(G\) be a finite connected simple graph and let \(\Delta\) be its maximum degree: every vertex of \(G\) has degree at most \(\Delta\) and some vertex has degree exactly \(\Delta\). If \(G\) is not complete and is not isomorphic to a cycle graph on an odd number of vertices, then \(G\) has a proper vertex coloring with \(\Delta\) colors.

theorem brooks {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (Δ : ℕ) (hconn : G.Connected)
    (hΔ : ∀ v, G.degree v ≤ Δ)
    (hΔatt : ∃ v, G.degree v = Δ)
    (hcomp : ¬Nonempty (G ≃g (⊤ : SimpleGraph V)))
    (hodd : ∀ (n : ℕ), Odd n → ¬Nonempty (G ≃g SimpleGraph.cycleGraph n)) :
    ∃ f : V → Fin Δ, ∀ ⦃v w : V⦄, G.Adj v w → f v ≠ f w

Sources

• R. L. Brooks, On colouring the nodes of a network, Proc. Camb. Philos. Soc. 37 (1941), DOI 10.1017/S030500410002168X.

TheoremErdős's theorem on graphs of high girth and high chromatic number#✓fully proved

For all natural numbers \(k\) and \(g\) with \(g \ge 3\), there is a finite simple graph \(G\) that has a cycle, whose girth (the length of a shortest cycle) is at least \(g\), and whose chromatic number is at least \(k\).

In particular, there are finite graphs of arbitrarily high girth and chromatic number.

theorem erdos_high_girth_chromatic (k g : ℕ) (hg : 3 ≤ g) :
    ∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V) (G : SimpleGraph V),
      g ≤ G.girth ∧ (k : ℕ∞) ≤ G.chromaticNumber

Sources

• P. Erdős, Graph theory and probability, Canad. J. Math. 11 (1959), 34–38, DOI 10.4153/CJM-1959-003-9.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.