Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local ...
summary
Presents a reusable Isabelle/HOL framework that formalises probabilistic existence proofs and gives the first machine-checked proof of the Lovász Local Lemma; builds a hierarchy of locales to package probability-space setup so typical proofs become one-line interprets plus calculation goals; proves several reusable probability lemmas and the often-omitted mutual independence principle used in combinatorics; uncovers an Isabelle probability-library issue (probability space vs universal set) and uses hypergraph colouring examples to show the approach improves automation and reuse.
AI-written summary · about
chapters (11)
- 0:00Probabilistic method intro
- 1:02What is probabilistic method
- 3:50Probabilistic proof framework
- 11:09Probabilistic proof calculations
- 12:32Lovász Local Lemma formalized
- 15:40Framework applications
- 19:35Key formalization insights
- 22:21Isabelle prob library challenges
- 23:46Generality in formalization
- 25:30Contributions and future work
- 26:13Q&A