利用洛瓦兹局部引理的形式化概率方法处理组合结构
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
AI总结：
本文提出在 Isabelle/HOL 中基于 locale 的模块化框架，首次形式化洛瓦兹局部引理，用于形式化组合结构存在性的概率证明，并通过超图着色经典引理验证其适用性。
摘要：
在过去五年中，组合数学的形式化库迅速扩展，但很少使用最重要的工具之一：概率。如何将关于组合结构（例如超图）存在性的直观概率论证转化为形式化文本？我们提出了一个在 Isabelle/HOL 中使用 locale 的模块化框架，用于形式化此类概率证明，包括基本存在性方法和洛瓦兹局部引理的首次形式化，这是概率论中的一个基本结果。该形式化侧重于适用于组合结构的通用、可复用的形式化概率引理，并指出了典型纸上直观概率推理中的几个显著空白。通过形式化几个关于具有特定着色超图存在性的经典引理，展示了这些技术的适用性。
英文摘要：
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ász 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
