### Abstract

This works presents a formalization of the Girth-Chromatic number theorem in graph theory, stating that graphs with arbitrarily large girth and chromatic number exist. The proof uses the theory of Random Graphs to prove the existence with probabilistic arguments.

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session Girth_Chromatic

- Girth_Chromatic_Misc
- Ugraphs
- Girth_Chromatic

### Used by

- Hypergraph Colouring Bounds
- Turán’s Graph Theorem
- Undirected Graph Theory
- Roth’s Theorem on Arithmetic Progressions
- Szemerédi’s Regularity Lemma
- Properties of Random Graphs – Subgraph Containment

## Cite

×

Girth_Chromatic-AFP

    @article{Girth_Chromatic-AFP,
      author  = {Lars Noschinski},
      title   = {A Probabilistic Proof of the Girth-Chromatic Number Theorem},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Girth_Chromatic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Feb 6, 2012 : Isabelle2011-1