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.

翻译：过去五年间，组合数学的形式化库迅速扩展，但极少利用概率这一重要工具。如何将常具直觉性的概率论证转换为形式化文本？我们提出Isabelle/HOL中的模块化框架，用于采用概率方法（如洛瓦斯局部引理，概率论中对存在性证明尤为重要的基础性结果）形式化组合证明。我们将该框架应用于超图着色中若干经典引理的形式化，揭示了直觉性概率推理如何可能误导数学家。