Combinatorial Design Theory

Chelsea Edmonds 🌐 and Lawrence C. Paulson 🌐

August 13, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Combinatorial design theory studies incidence set systems with certain balance and symmetry properties. It is closely related to hypergraph theory. This formalisation presents a general library for formal reasoning on incidence set systems, designs and their applications, including formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs. Notably, this includes formalising t-designs, balanced incomplete block designs (BIBD), group divisible designs (GDD), pairwise balanced designs (PBD), design isomorphisms, and the relationship between graphs and designs. A locale-centric approach has been used to manage the relationships between the many different types of designs. Theorems of particular interest include the necessary conditions for existence of a BIBD, Wilson's construction on GDDs, and Bose's inequality on resolvable designs. Parts of this formalisation are explored in the paper "A Modular First Formalisation of Combinatorial Design Theory", presented at CICM 2021.


BSD License


Session Design_Theory