A Modular First Formalisation of Combinatorial Design Theory
Chelsea Edmonds, Lawrence Paulson
TL;DR
The paper addresses the challenge of formalising combinatorial design theory in a proof assistant by introducing a modular, locale-centric formalisation in Isabelle/HOL. The authors build a scalable hierarchy from incidence systems to BIBDs and beyond, leveraging little theories, locale combinations, and interpretation to enable concise, reusable proofs. Key contributions include the first complete formalisation of design theory in Isabelle/HOL, a family of 36 design-related locales plus graph extensions, and proofs for constructions and parameter relations such as $r (k - 1) = Lambda (v - 1)$ and $v r = b k$. The work provides a reusable library with practical impact for rigorous combinatorial proofs and offers avenues to connect design theory with graph and hypergraph formalisations.
Abstract
Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and assesses the usability of a locale-centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to specify numerous types of designs and their hierarchy. The resulting library, which is concise and adaptable, includes formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs.