  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.

Logic in Computer Science;Combinatorics