Publications

Published Papers

2024

1. ACM

   Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma

   Chelsea Edmonds, and Lawrence C. Paulson

   In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs , London, UK, 2024

   Distinguished Paper Award Abs Bib HTML

   Top 10% of accepted papers

   Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial structures, such as hypergraphs, be translated into a formal text? We present a modular framework using locales in Isabelle/HOL to formalise such probabilistic proofs, including the basic existence method and first formalisation of the Lovász local lemma, a fundamental result in probability. The formalisation focuses on general, reusable formal probabilistic lemmas for combinatorial structures, and highlights several notable gaps in typical intuitive probabilistic reasoning on paper. The applicability of the techniques is demonstrated through the formalisation of several classic lemmas on the existence of hypergraphs with certain colourings.

   @inproceedings{10.1145/3636501.3636946,
     author = {Edmonds, Chelsea and Paulson, Lawrence C.},
     title = {Formal Probabilistic Methods for Combinatorial Structures using the Lov\'{a}sz Local Lemma},
     year = {2024},
     isbn = {9798400704888},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     doi = {10.1145/3636501.3636946},
     booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs},
     pages = {132–146},
     numpages = {15},
     keywords = {probability, hypergraph colourings, formalisation of mathematics, combinatorics, Lov\'{a}sz local lemma, Isabelle/HOL, Interactive theorem proving},
     location = {London, UK},
     series = {CPP 2024},
   }

2023

1. ACM

   A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL

   Angeliki Koutsoukou-Argyraki , Mantas Bakšys , and Chelsea Edmonds

   In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs , Boston, MA, USA, 2023

   Abs Bib HTML

   We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemerédi–Gowers Theorem, a profound result in additive combinatorics which played a central role in Gowers’s proof deriving the first effective bounds for Szemerédi’s Theorem. The proof is of great mathematical interest given that it involves an interplay between different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics involving algebraic objects. This interplay is what made the process of the formalisation, for which we had to develop formalisations of new background material in the aforementioned areas, more rich and technically challenging. We demonstrate how locales, Isabelle’s module system, can be employed to handle such interplays in mathematical formalisations. To treat the graph-theoretic aspects of the proof, we make use of a new, more general undirected graph theory library developed by Edmonds, which is both flexible and extensible. In addition to the main theorem, which, following our source, is formulated for difference sets, we also give an alternative version for sumsets which required a formalisation of an auxiliary triangle inequality. We moreover formalise a few additional results in additive combinatorics that are not used in the proof of the main theorem. This is the first formalisation of the Balog–Szemerédi–Gowers Theorem in any proof assistant to our knowledge.

   @inproceedings{10.1145/3573105.3575680,
     author = {Koutsoukou-Argyraki, Angeliki and Bak\v{s}ys, Mantas and Edmonds, Chelsea},
     title = {A Formalisation of the Balog–Szemer\'{e}di–Gowers Theorem in Isabelle/HOL},
     year = {2023},
     isbn = {9798400700262},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     doi = {10.1145/3573105.3575680},
     booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs},
     pages = {225–238},
     numpages = {14},
     keywords = {proof assistant, probabilistic method, interactive theorem proving, graph theory, formalisation of mathematics, additive combinatorics, Isabelle/HOL},
     location = {Boston, MA, USA},
     series = {CPP 2023},
   }

2022

1. JAR

   Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

   Chelsea Edmonds, Angeliki Koutsoukou-Argyraki , and Lawrence C. Paulson

   Journal of Automated Reasoning, Dec 2022

   Abs Bib HTML

   We have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.

   @article{10.1007/s10817-022-09650-2,
     author = {Edmonds, Chelsea and Koutsoukou-Argyraki, Angeliki and Paulson, Lawrence C.},
     title = {Formalising Szemer\'{e}di’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL},
     year = {2022},
     issue_date = {Mar 2023},
     publisher = {Springer-Verlag},
     address = {Berlin, Heidelberg},
     volume = {67},
     number = {1},
     issn = {0168-7433},
     doi = {10.1007/s10817-022-09650-2},
     journal = {Journal of Automated Reasoning},
     month = dec,
     numpages = {21},
     keywords = {68V35, 68V20, 68V15, 03B35, 11P81, 05A17, 05C35, Number theory, Arithmetic progressions, Extremal graph theory, Additive combinatorics, Isabelle/HOL, Formalisation of mathematics, Proof assistant, Interactive theorem proving}
   }

2. LIPIcs

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

   Chelsea Edmonds, and Lawrence C. Paulson

   In 13th International Conference on Interactive Theorem Proving (ITP 2022) , Dec 2022

   Abs Bib HTML

   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.

   @inproceedings{edmondsfishers2022,
     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)},
     year = {2022},
     volume = {237},
     editor = {Andronick, June and de Moura, Leonardo},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     address = {Dagstuhl, Germany},
     doi = {10.4230/LIPIcs.ITP.2022.11},
     annote = {Keywords: Isabelle/HOL, Mathematical Formalisation, Fisher’s Inequality, Linear Algebra, Formal Proof Techniques, Combinatorics},
   }

2021

1. LNCS

   A Modular First Formalisation of Combinatorial Design Theory

   Chelsea Edmonds, and Lawrence C. Paulson

   In Intelligent Computer Mathematics: 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings , Timisoara, Romania, Dec 2021

   Abs Bib HTML

   Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and assesses the usability of a locale-centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to specify numerous types of designs and their hierarchy. The resulting library, which is concise and adaptable, includes formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs.

   @inproceedings{10.1007/978-3-030-81097-9_1,
     author = {Edmonds, Chelsea and Paulson, Lawrence C.},
     title = {A Modular First Formalisation of Combinatorial Design Theory},
     year = {2021},
     isbn = {978-3-030-81096-2},
     publisher = {Springer-Verlag},
     address = {Berlin, Heidelberg},
     doi = {10.1007/978-3-030-81097-9_1},
     booktitle = {Intelligent Computer Mathematics: 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings},
     pages = {3–18},
     numpages = {16},
     keywords = {Locales, Block designs, Combinatorial design theory, Interactive proof assistants, Formalisation, Combinatorics, Isabelle/HOL},
     location = {Timisoara, Romania},
   }

Workshop Papers

2020

1. Isabelle

   Lucas’s Theorem: Formalising Generating Function Proofs

   Chelsea Edmonds

   In Isabelle Workshop 2020, associated with IJCAR2020 , 2020

   HTML

AFP Entries

2023

1. 

   Hypergraph Colouring Bounds

   Chelsea Edmonds, and Lawrence C. Paulson

   Archive of Formal Proofs, Sep 2023

   Formal Proof Development

   Bib HTML

   @article{Hypergraph_Colourings-AFP,
     author = {Edmonds, Chelsea and Paulson, Lawrence C.},
     title = {Hypergraph Colouring Bounds},
     journal = {Archive of Formal Proofs},
     month = sep,
     year = {2023},
     note = {Formal Proof Development},
   }

2. 

   Hypergraphs

   Chelsea Edmonds

   Archive of Formal Proofs, Sep 2023

   Formal Proof Development

   Bib HTML

   @article{Hypergraph_Basics-AFP,
     author = {Edmonds, Chelsea},
     title = {Hypergraphs},
     journal = {Archive of Formal Proofs},
     month = sep,
     year = {2023},
     note = {Formal Proof Development},
   }

3. 

   General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma

   Chelsea Edmonds

   Archive of Formal Proofs, Sep 2023

   Formal Proof Development

   Bib HTML

   @article{Lovasz_Local-AFP,
     author = {Edmonds, Chelsea},
     title = {General {Probabilistic Techniques} for {Combinatorics} and the {Lovasz Local Lemma}},
     journal = {Archive of Formal Proofs},
     month = sep,
     year = {2023},
     note = {Formal Proof Development},
   }

2022

1. 

   The Balog–Szemerédi–Gowers Theorem

   Angeliki Koutsoukou-Argyraki , Mantas Bakšys , and Chelsea Edmonds

   Archive of Formal Proofs, Nov 2022

   Formal Proof Development

   Bib HTML

   @article{Balog_Szemeredi_Gowers-AFP,
     author = {Koutsoukou-Argyraki, Angeliki and Bakšys, Mantas and Edmonds, Chelsea},
     title = {The {Balog–Szemerédi–Gowers Theorem}},
     journal = {Archive of Formal Proofs},
     month = nov,
     year = {2022},
     note = {Formal Proof Development},
   }

2. 

   Undirected Graph Theory

   Chelsea Edmonds

   Archive of Formal Proofs, Sep 2022

   Formal Proof Development

   Bib HTML

   @article{Chelsea_Graph_AFP,
     author = {Edmonds, Chelsea},
     title = {Undirected {Graph Theory}},
     journal = {Archive of Formal Proofs},
     month = sep,
     year = {2022},
     note = {Formal Proof Development},
   }

3. 

   Fisher’s Inequality: Linear Algebraic Proof Techniques for Combinatorics

   Chelsea Edmonds, and Lawrence C. Paulson

   Archive of Formal Proofs, Apr 2022

   Formal Proof Development

   Bib HTML

   @article{Fishers_Inequality-AFP,
     author = {Edmonds, Chelsea and Paulson, Lawrence C.},
     title = {{Fisher's Inequality}: {Linear Algebraic Proof Techniques} for {Combinatorics}},
     journal = {Archive of Formal Proofs},
     month = apr,
     year = {2022},
     note = {Formal Proof Development},
   }

2021

1. 

   Szemerédi’s Regularity Lemma

   Chelsea Edmonds, Angeliki Koutsoukou-Argyraki , and Lawrence C. Paulson

   Archive of Formal Proofs, Nov 2021

   Formal Proof Development

   Bib HTML

   @article{Szemeredi_Regularity-AFP,
     author = {Edmonds, Chelsea and Koutsoukou-Argyraki, Angeliki and Paulson, Lawrence C.},
     title = {Szemerédi's {Regularity Lemma}},
     journal = {Archive of Formal Proofs},
     month = nov,
     year = {2021},
     note = {Formal Proof Development},
   }

2. 

   Roth’s Theorem on Arithmetic Progressions

   Chelsea Edmonds, Angeliki Koutsoukou-Argyraki , and Lawrence C. Paulson

   Archive of Formal Proofs, Dec 2021

   Formal Proof Development

   Bib HTML

   @article{Roth_Arithmetic_Progressions-AFP,
     author = {Edmonds, Chelsea and Koutsoukou-Argyraki, Angeliki and Paulson, Lawrence C.},
     title = {Roth's {Theorem} on {Arithmetic Progressions}},
     journal = {Archive of Formal Proofs},
     month = dec,
     year = {2021},
     note = {Formal Proof Development},
   }

3. 

   Combinatorial Design Theory

   Chelsea Edmonds, and Lawrence C. Paulson

   Archive of Formal Proofs, Aug 2021

   Formal Proof Development

   Bib HTML

   @article{Design_Theory-AFP,
     author = {Edmonds, Chelsea and Paulson, Lawrence C.},
     title = {Combinatorial {Design Theory}},
     journal = {Archive of Formal Proofs},
     month = aug,
     year = {2021},
     note = {Formal Proof Development},
   }

2020

1. 

   Lucas’s Theorem

   Chelsea Edmonds

   Archive of Formal Proofs, Apr 2020

   Formal Proof Development

   Bib HTML

   @article{Lucas_Theorem-AFP,
     author = {Edmonds, Chelsea},
     title = {Lucas's {Theorem}},
     journal = {Archive of Formal Proofs},
     month = apr,
     year = {2020},
     note = {Formal Proof Development},
   }

Theses

2023

1. PhD Thesis

   Formalising Combinatorial Structures and Proof Techniques in Isabelle/HOL

   Chelsea Edmonds

   Apollo - University of Cambridge Repository , 2023

   Bib HTML

   @phdthesis{edmonds_2023,
     title = {Formalising Combinatorial Structures and Proof Techniques in Isabelle/HOL},
     doi = {10.17863/CAM.108886},
     school = {Apollo - University of Cambridge Repository},
     author = {Edmonds, Chelsea},
     year = {2023},
     keywords = {Isabelle/HOL, Formalisation of Mathematics},
   }