Document Open Access Logo

Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics

Authors Chelsea Edmonds , Lawrence C. Paulson

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.11.pdf
  • Filesize: 0.68 MB
  • 19 pages

Document Identifiers

Author Details

Chelsea Edmonds
  • Department of Computer Science and Technology, University of Cambridge, UK
Lawrence C. Paulson
  • Department of Computer Science and Technology, University of Cambridge, UK

Funding

  • Edmonds, Chelsea: Funded jointly by the Cambridge Trust (Cambridge Australia Scholarship) and a Cambridge Department of Computer Science Qualcomm Premium Research Scholarship.
  • Paulson, Lawrence C.: Supported by the ERC Advanced Grant ALEXANDRIA (Project GA 742178).

Acknowledgements

Thanks to Wenda Li, for the helpful pointers on working with linear algebra in Isabelle, and Yiannos Stathopoulos, for the suggestions on utilising SErAPIS to navigate results from past formalisations.

Cite AsGet BibTex

Chelsea Edmonds and Lawrence C. Paulson. Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.11

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Higher order logic
  • Mathematics of computing → Combinatorics
Keywords
  • Isabelle/HOL
  • Mathematical Formalisation
  • Fisher’s Inequality
  • Linear Algebra
  • Formal Proof Techniques
  • Combinatorics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Jesús Aransay and Jose Divasón. Formalization and Execution of Linear Algebra: From Theorems to Algorithms. In Gopal Gupta and Ricardo Peña, editors, Logic-Based Program Synthesis and Transformation, volume 8901, pages 1-18. Springer International Publishing, Cham, 2014. Google Scholar
  2. László Babai and Péter Frankl. Linear Algebra Methods in Combinatorics. Department of Computer Science, University of Chicago, 2.1 edition, 2020. URL: https://people.cs.uchicago.edu/~laci/CLASS/HANDOUTS-COMB/BaFrNew.pdf.
  3. Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, Lecture Notes in Computer Science, pages 34-50, Berlin, Heidelberg, 2004. Springer. Google Scholar
  4. R. C. Bose. A Note on Fisher’s Inequality for Balanced Incomplete Block Designs. The Annals of Mathematical Statistics, 20(4):619-620, December 1949. Google Scholar
  5. Richard A. Brualdi and Herbert J. Ryser. Combinatorial Matrix Theory. Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1991. Google Scholar
  6. Boris Bukh. Lecture notes in algebraic Methods in Combinatorics: Rank argument, 2014. URL: http://www.borisbukh.org/AlgMethods14/rank_notes.pdf.
  7. C. J Colbourn and Jeffrey H. Dinitz. Handbook of Combinatorial Designs / Edited by Charles J. Colbourn, Jeffrey H. Dinitz. Discrete Mathematics and Its Applications. Chapman & Hall/CRC, Boca Raton, Fla. ; London, 2nd ed. edition, 2007. Google Scholar
  8. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, and Akihisa Yamada. A Verified Implementation of the BerlekampendashZassenhaus Factorization Algorithm. Journal of Automated Reasoning, 64(4):699-735, April 2020. Google Scholar
  9. Chelsea Edmonds and Lawrence C. Paulson. A Modular First Formalisation of Combinatorial Design Theory. In CICM, 2021. Google Scholar
  10. R. A. Fisher. An Examination of the Different Possible Solutions of a Problem in Incomplete Blocks. Annals of Eugenics, 10(1):52-75, 1940. Google Scholar
  11. P. Frankl and R. M. Wilson. Intersection theorems with geometric consequences. Combinatorica, 1(4):357-368, December 1981. Google Scholar
  12. C. D. Godsil. Tools from Linear Algebra. In Lovász L Graham RL, Grötschel M, editor, Handbook of Combinatorics, volume 2. Elsevier, Amsterdam, 1996. Google Scholar
  13. Georges Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In Deepak Kapur, editor, Computer Mathematics, Lecture Notes in Computer Science, pages 333-333, Berlin, Heidelberg, 2008. Springer. Google Scholar
  14. W. T. Gowers. Dimension arguments in combinatorics, July 2008. URL: https://gowers.wordpress.com/2008/07/31/dimension-arguments-in-combinatorics/.
  15. John Harrison. The hol light theory of euclidean space. J. Autom. Reason., 50(2):173-190, February 2013. URL: https://doi.org/10.1007/s10817-012-9250-9.
  16. Brian Huffman and Ondřej Kunčar. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, Georges Gonthier, and Michael Norrish, editors, Certified Programs and Proofs, volume 8307, pages 131-146. Springer International Publishing, Cham, 2013. Google Scholar
  17. Stasys Jukna. Extremal Combinatorics. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. Google Scholar
  18. Jonas Keinholz. Matroids. Isabelle Archive of Formal Proofs, November 2018. URL: https://www.isa-afp.org/entries/Matroids.html.
  19. Daniel Kroes, Jacob Naranjo, Jiaxi Nie, Jason O'Neill, Nicholas Sieger, Sam Sprio, and Emily Zhu. Lecture notes: Linear Algebra methods in Combinatorics, 2019. URL: https://mathweb.ucsd.edu/~sspiro/Abacus/AbacusF19.pdf.
  20. Kulendra N. Majumdar. On some Theorems in Combinatorics Relating to Incomplete Block Designs. The Annals of Mathematical Statistics, 24(3):377-389, September 1953. Google Scholar
  21. Lars Noschinski. A Graph Library for Isabelle. Mathematics in Computer Science, 9(1):23-39, March 2015. Google Scholar
  22. Steven Obua and Technische Universität München. Proving bounds for real linear programs in isabelle/HOL. In Theorem Proving in Higher Order Logics (TPHOLs 2005), Volume 3603 of Lect. Notes in Comp. Sci, pages 227-244. Springer, 2005. Google Scholar
  23. Leonard H. Soicher. Design GAP Manual. URL: https://www.gap-system.org/Manuals/pkg/design-1.7/doc/manual.pdf.
  24. Douglas Stinson. Combinatorial Designs: Constructions and Analysis. Springer-Verlag, New York, 2004. Google Scholar
  25. René Thiemann and Akihisa Yamada. Formalizing Jordan normal forms in Isabelle/HOL. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 88-99, St. Petersburg, FL, USA, January 2016. Association for Computing Machinery. Google Scholar
  26. Markus Wenzel. Isabelle, Isar - A Versatile Environment for Human Readable Formal Proof Documents. PhD thesis, Technical University Munich, Germany, 2002. URL: http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact