Formalising Combinatorial Structures and Proof Techniques in Isabelle/HOL

Abstract

The formalisation of mathematics is an area of increasing interest, enabling us to verify correctness, gain deeper insight into proofs, and benefit from advances in automation and search. The remarkable growth over the last decade in proof assistant capabilities and advanced formal mathematical libraries has seen the field reach an exciting new stage. Formalisation has the potential to change how mathematical research is done, while from a computer science perspective, formalised mathematics provides a basis for the formal verification of many applications. Until recently combinatorics was a comparatively undeveloped field in formal mathematical libraries, despite its many critical computing applications. This thesis presents the first formalisations of numerous combinatorial structures and generalised formal proof techniques for combinatorics using the proof assistant Isabelle/HOL. These, in turn, explore the interplay between different mathematical fields in a formal environment. The thesis begins with an outline of the locale-centric approach for formalising complex hierarchies, inspired by Ballarin and further explored through this work. The approach and proof techniques are demonstrated through the formalisation of complex overlapping hierarchies of combinatorial structures, including aspects of graph theory, hypergraph theory, and combinatorial design theory. There is a particular focus on design theory, which had not previously been formalised in any system. The remaining chapters focus on the formalisation of three categories of proof techniques: traditional combinatorial techniques such as counting and generating functions, algebraic techniques, and probabilistic techniques. In each chapter, the thesis details the general formal techniques and frameworks developed, as well as their successful application to formalising numerous theorems on the construction and existence of combinatorial structures. Additionally, the thesis highlights my individual contributions to collaborations which resulted in the formalisation of several significant combinatorial theorems, namely Szemerédi's regularity lemma, Roth's theorem on arithmetic progressions, and the Balog-Szemerédi-Gowers theorem. Through this work, I aim to present a new approach to mathematical formalisation which focuses on developing general, modular formal proof techniques and modelling approaches, rather than purely verifying theorems. Ultimately, this research intends to improve the accessibility of formalising mathematics in Isabelle/HOL through significant modular, flexible, and extensible libraries and frameworks.