Proof pearl: a probabilistic proof for the girth-chromatic number theorem. (English) Zbl 1360.68763

Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 393-404 (2012).
Summary: The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chromatic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a standard textbook proof and use this to explore the use of the probabilistic method in a theorem prover.
For the entire collection see [Zbl 1246.68023].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
05-04 Software, source code, etc. for problems pertaining to combinatorics
05C15 Coloring of graphs and hypergraphs
05C38 Paths and cycles
Full Text: DOI