Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
Chelsea Edmonds, Lawrence C. Paulson
TL;DR
The paper tackles the challenge of formalising combinatorial proofs by developing formal linear-algebraic representations of incidence set systems in Isabelle/HOL, and applies them to the first formalisation of Fisher's inequality, i.e., a bound $m \le n$ for incidence systems with constant intersection. It formalises incidence matrices and develops rank-argument and linear-bound techniques, plus variations of Fisher's inequality, as a foundation for broader combinatorial formalisation. By building on prior work in design theory and linear algebra libraries, the approach aims to generalise proof patterns and enable reuse across diverse combinatorial settings. The results demonstrate the practicality and benefits of a linear-algebraic formalisation path for combinatorics, complementing traditional proofs and enabling cross-field verifications.
Abstract
The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher's inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher's inequality.