Lucas's Theorem. - Chelsea Edmonds (Arch. Formal Proofs, 2020)

A Modular First Formalisation of Combinatorial Design Theory. - Chelsea Edmonds; Lawrence C. Paulson (CICM, 2021)

Szemerédi's Regularity Lemma. - Chelsea Edmonds; Angeliki Koutsoukou-Argyraki; Lawrence C. Paulson (Arch. Formal Proofs, 2021)

Roth's Theorem on Arithmetic Progressions. - Chelsea Edmonds; Angeliki Koutsoukou-Argyraki; Lawrence C. Paulson (Arch. Formal Proofs, 2021)

Combinatorial Design Theory. - Chelsea Edmonds; Lawrence C. Paulson (Arch. Formal Proofs, 2021)

Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. - Chelsea Edmonds; Lawrence C. Paulson (ITP, 2022)

Undirected Graph Theory. - Chelsea Edmonds (Arch. Formal Proofs, 2022)

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics. - Chelsea Edmonds; Lawrence C. Paulson (Arch. Formal Proofs, 2022)

The Balog-Szemerédi-Gowers Theorem. - Angeliki Koutsoukou-Argyraki; Mantas Baksys; Chelsea Edmonds (Arch. Formal Proofs, 2022)

A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. - Angeliki Koutsoukou-Argyraki; Mantas Baksys; Chelsea Edmonds (CPP, 2023)

General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma. - Chelsea Edmonds (Arch. Formal Proofs, 2023)

Hypergraphs. - Chelsea Edmonds (Arch. Formal Proofs, 2023)

Hypergraph Colouring Bounds. - Chelsea Edmonds; Lawrence C. Paulson (Arch. Formal Proofs, 2023)

Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. - Chelsea Edmonds; Lawrence C. Paulson (CoRR, 2023)

Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. - Chelsea Edmonds; Angeliki Koutsoukou-Argyraki; Lawrence C. Paulson (J. Autom. Reason., 2023)

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. - Chelsea Edmonds; Lawrence C. Paulson (CPP, 2024)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)