Formal Probabilistic Methods for Combinatorial Structures using the Lov\'asz Local Lemma

TL;DR

This paper introduces a modular formal framework in Isabelle/HOL for probabilistic proofs in combinatorics, including the Lovász Local Lemma, enabling rigorous verification of probabilistic existence arguments.

Contribution

It presents the first formalisation of the Lovász Local Lemma in Isabelle/HOL and develops reusable probabilistic lemmas for combinatorial structures.

Findings

Formalised the Lovász Local Lemma in Isabelle/HOL

Developed reusable probabilistic lemmas for combinatorics

Verified existence of hypergraphs with specific colourings

Abstract

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 on the existence of combinatorial structures, such as hypergraphs, be translated into a formal text? We present a modular framework using locales in Isabelle/HOL to formalise such probabilistic proofs, including the basic existence method and first formalisation of the Lov\'asz local lemma, a fundamental result in probability. The formalisation focuses on general, reusable formal probabilistic lemmas for combinatorial structures, and highlights several notable gaps in typical intuitive probabilistic reasoning on paper. The applicability of the techniques is demonstrated through the formalisation of several classic lemmas on the existence of hypergraphs with certain colourings.