Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments be translated into a formal text? We present a modular framework in Isabelle/HOL to formalise combinatorial proofs using probabilistic methods such as the Lov\'asz local lemma, a fundamental result in probability which is particularly important for existence proofs. We apply the framework to formalise several classic lemmas on hypergraph colourings, revealing how intuitive probabilistic reasoning can lead mathematicians astray.

翻译：暂无翻译