License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.11
URN: urn:nbn:de:0030-drops-167204
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16720/
Edmonds, Chelsea ;
Paulson, Lawrence C.
Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
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.
BibTeX - Entry
@InProceedings{edmonds_et_al:LIPIcs.ITP.2022.11,
author = {Edmonds, Chelsea and Paulson, Lawrence C.},
title = {{Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16720},
URN = {urn:nbn:de:0030-drops-167204},
doi = {10.4230/LIPIcs.ITP.2022.11},
annote = {Keywords: Isabelle/HOL, Mathematical Formalisation, Fisher’s Inequality, Linear Algebra, Formal Proof Techniques, Combinatorics}
}
