Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
From MaRDI portal
Publication:6506201
DOI10.4230/LIPICS.ITP.2022.11arXiv2207.02728MaRDI QIDQ6506201FDOQ6506201
Authors: Chelsea Edmonds, Lawrence C. Paulson 
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.
Combinatorial aspects of block designs (05B05) Combinatorial aspects of matrices (incidence, Hadamard, etc.) (05B20) Extremal set theory (05D05) Formalization of mathematics in connection with theorem provers (68V20)
This page was built for publication: Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6506201)
