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.

翻译：过去五年中，组合数学的形式化库迅速扩展，但其中鲜少涉及最重要的工具之一：概率论。如何将关于组合结构（如超图）存在性的直观概率论证转化为形式化文本？我们提出一个基于Isabelle/HOL中区域（locales）的模块化框架，用于形式化此类概率证明，包括基本存在性方法以及概率论基础成果Lovász局部引理的首次形式化。该形式化聚焦于为组合结构构建通用、可复用的形式化概率引理，并揭示了典型纸面概率直觉推理中的若干显著空白。通过形式化若干关于特定着色超图存在性的经典引理，展示了该技术的实用性。