Publications | Chelsea L. Edmonds

Published Papers

2024

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

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

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}
}

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

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}, }

2020

Workshop

Lucas’s Theorem: Formalising Generating Function Proofs

Chelsea Edmonds

In Isabelle Workshop 2020, associated with IJCAR2020 , Dec 2020

HTML

AFP Entries

2023

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},
}

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},
}

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

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},
}

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},
}

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

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},
}

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},
}

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

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},
}