@article{Chelsea_Graph_AFP,
  author  = {Chelsea Edmonds},
  title   = {Undirected Graph Theory},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Undirected_Graph_Theory.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{noschinskiGraphLibrary2015,
  title    = {A {{Graph Library}} for {{Isabelle}}},
  author   = {Noschinski, Lars},
  year     = {2015},
  month    = mar,
  volume   = {9},
  pages    = {23--39},
  issn     = {1661-8270, 1661-8289},
  doi      = {10.1007/s11786-014-0183-z},
  journal  = {Mathematics in Computer Science},
  language = {en},
  number   = {1}
}

@inproceedings{edmonds-modular-first,
  abstract      = {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.},
  author        = {Edmonds, Chelsea and Paulson, Lawrence C.},
  booktitle     = {Intelligent Computer Mathematics},
  date-added    = {2022-03-11 16:43:43 +0000},
  date-modified = {2022-03-11 16:43:43 +0000},
  editor        = {Kamareddine, Fairouz and Sacerdoti Coen, Claudio},
  isbn          = {978-3-030-81096-2},
  pages         = {3-18},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  location = {Timisoara, Romania},
  title         = {A Modular First Formalisation of Combinatorial Design Theory},
  year          = {2021},
  doi           = {https://doi.org/10.1007/978-3-030-81097-9_1}
}

@inproceedings{DilliesMehta,
author ={Dillies, Ya\"{e}l and Mehta, Bhavik},
  title ={{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
  booktitle ={13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages ={9:1--9: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/16718},
  URN ={urn:nbn:de:0030-drops-167185},
  doi ={10.4230/LIPIcs.ITP.2022.9},
}

@book{IsabelleBook,
  author    = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  note      = {Online at \url{http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf}},
  publisher = {Springer},
  title     = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
  year      = {2002}
}

@book{molloy2002graph,
  title = {Graph Colouring and the Probabilistic Method},
  author = {Molloy, M. and Reed, B.},
  year = {2002},
  series = {Algorithms and Combinatorics},
  publisher = {{Springer}},
  url = {https://books.google.co.uk/books?id=GH9udeCZ758C},
  isbn = {978-3-540-42139-9},
  lccn = {2001055101}
}


@misc{Zhaonotes,
  author = {Zhao, Yufei},
  note   = {Lecture notes MIT 18.226, Fall 2020, \url{https://ocw.mit.edu/courses/18-226-probabilistic-method-in-combinatorics-fall-2020/resources/mit18_226f20_full_notes/}},
  title  = {Probabilistic Methods in Combinatorics},
  year   = {2020}
}

@inproceedings{MehtaKruskal,
author = {Mehta, Bhavik},
title = {Formalising the Kruskal-Katona Theorem in Lean},
year = {2022},
isbn = {978-3-031-16680-8},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
url = {https://doi.org/10.1007/978-3-031-16681-5_5},
doi = {10.1007/978-3-031-16681-5_5},
abstract = {The Kruskal-Katona theorem is a celebrated result of extremal combinatorics providing precise cardinality bounds on the ‘shadow’ of a family of finite sets: the family given by removing an element from each set of the original. We describe a formalisation of the Kruskal-Katona theorem in the Lean theorem prover, including a computable implementation of the shadow as well as standard inequalities about it, and a definition of the colexicographic ordering on finite sets. In addition, we apply these results to other classical combinatorial theorems: Sperner’s theorem on antichains and the Erd\H{o}s-Ko-Rado theorem on intersecting families.},
booktitle = {Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings},
pages = {75–91},
numpages = {17},
keywords = {Extremal combinatorics, Formalisation, Lean Theorem Prover},
location = {Tbilisi, Georgia}
}

@inproceedings{SErAPIS2,
  author    = {Yiannos Stathopoulos and Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
  title     = {Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges  },
  note      = {Informal proceedings},
  booktitle = {5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France},
  year      = {2020},
  publisher = {},
  url  = {http://aitp-conference.org/2020/abstract/paper_9.pdf}
}

@article{ballarinExploringStructureAlgebra2020,
	abstract = {Locales, the module system of the theorem prover Isabelle, were designed so that developments in abstract algebra could be represented faithfully and concisely. Whether these goals were met is assessed through a case study. Parts of an algebra textbook, Jacobson's Basic Algebra, that are challenging structurally were formalised. Key parts of the formalisation are presented in greater detail. An analysis of the work from both qualitative and quantitative perspectives substantiates that the design goals were met. In particular, the size ratio of formal to ``pen and paper'' text does not increase when going further into the book. The analysis also yields guidance on locales including patterns of use, which are identified and described.},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  doi = {https://doi.org/10.1007/s10817-019-09537-9},
	author = {Ballarin, Clemens},
	date-modified = {2021-03-22 15:52:21 +0000},
	file = {C\:\\Users\\cledm\\Zotero\\storage\\43ZDK9EK\\Exploring the Structure of an Algebra Text with Locales SpringerLink.pdf},
	issn = {0168-7433},
	journal = {Journal of Automated Reasoning},
	month = {August},
	number = {6},
	pages = {1093-1121},
	title = {Exploring the {{Structure}} of an {{Algebra Text}} with {{Locales}}},
	volume = {64},
	year = {2020}}

  @incollection{ballarinInterpretationLocalesIsabelle2006,
	abstract = {The generic proof assistant Isabelle provides a landscape of specification contexts that is considerably richer than that of most other provers. Theories are the level of specification where object-logics are axiomatised. Isabelle's proof language Isar enables local exploration in contexts generated in the course of natural deduction proofs. Finally, locales, which may be seen as detached proof contexts, offer an intermediate level of specification geared towards reuse. All three kinds of contexts are structured, to different extents. We analyse the ``topology'' of Isabelle's landscape of specification contexts, by means of development graphs, in order to establish what kinds of reuse are possible.},
	address = {{Berlin, Heidelberg}},
	author = {Ballarin, Clemens},
	booktitle = {Mathematical {{Knowledge Management}}},
	editor = {Hutchison, David and Kanade, Takeo and Kittler, Josef and Kleinberg, Jon M. and Mattern, Friedemann and Mitchell, John C. and Naor, Moni and Nierstrasz, Oscar and Pandu Rangan, C. and Steffen, Bernhard and Sudan, Madhu and Terzopoulos, Demetri and Tygar, Dough and Vardi, Moshe Y. and Weikum, Gerhard and Borwein, Jonathan M. and Farmer, William M.},
	file = {C\:\\Users\\cledm\\Zotero\\storage\\4Y8AIYV4\\Ballarin - 2006 - Interpretation of Locales in Isabelle Theories an.pdf},
	isbn = {978-3-540-37104-5 978-3-540-37106-9},
	keywords = {locales},
	language = {en},
	note = {\url{http://link.springer.com/10.1007/11812289_4}},
	pages = {31--43},
	publisher = {{Springer Berlin Heidelberg}},
	shorttitle = {Interpretation of {{Locales}} in {{Isabelle}}},
	title = {Interpretation of {{Locales}} in {{Isabelle}}: {{Theories}} and {{Proof Contexts}}},
	volume = {4108},
	year = {2006}}

@inproceedings{ballarinLocalesLocaleExpressions2004,
	abstract = {Locales provide a module system for the Isabelle proof assistant. Recently, locales have been ported to the new Isar format for structured proofs. At the same time, they have been extended by locale expressions, a language for composing locale specifications, and by structures, which provide syntax for algebraic structures. The present paper presents both and is suitable as a tutorial to locales in Isar, because it covers both basics and recent extensions, and contains many examples.},
	author = {Ballarin, Clemens},
	booktitle = {Types for {{Proofs}} and {{Programs}}},
	date-modified = {2021-03-22 15:39:41 +0000},
	editor = {Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
	file = {C\:\\Users\\cledm\\Zotero\\storage\\7CGU24CE\\Ballarin_2004_Locales and Locale Expressions in Isabelle-Isar.pdf},
	isbn = {978-3-540-24849-1},
	keywords = {Context Element,Locale Expression,Locale Predicate,Locale Semi,Note Element},
	language = {en},
	pages = {34--50},
	publisher = {{Springer}},
	series = {LNCS 3085},
	title = {Locales and {{Locale Expressions}} in {{Isabelle}}/{{Isar}}},
	year = {2004}}

@article{ballarinLocalesModuleSystem2014,
	abstract = {Locales are a module system for managing theory hierarchies in a theorem prover through theory interpretation. They are available for the theorem prover Isabelle. In this paper, their semantics is defined in terms of local theories and morphisms. Locales aim at providing flexible means of extension and reuse. Theory modules (which are called locales) may be extended by definitions and theorems. Interpretation to Isabelle's global theories and proof contexts is possible via morphisms. Even the locale hierarchy may be changed if declared relations between locales do not adequately reflect logical relations, which are implied by the locales' specifications. By discussing their design and relating it to more commonly known structuring mechanisms of programming languages and provers, locales are made accessible to a wider audience beyond the users of Isabelle. The discussed mechanisms include ML-style functors, type classes and mixins (the latter are found in modern object-oriented languages).},
	author = {Ballarin, Clemens},
	file = {C\:\\Users\\cledm\\Zotero\\storage\\3J6I5SY7\\Ballarin_2014_Locales.pdf},
	issn = {1573-0670},
	journal = {Journal of Automated Reasoning},
	language = {en},
	month = feb,
	note = {\url{https://doi.org/10.1007/s10817-013-9284-7}},
	number = {2},
	pages = {123--153},
	shorttitle = {Locales},
	title = {Locales: {{A Module System}} for {{Mathematical Theories}}},
	volume = {52},
	year = {2014}}

@incollection{ballarinTutorialLocalesLocale2010a,
	author = {Ballarin, Clemens},
	booktitle = {Contribuciones {Cient\'ificas} en Honor de Mirian {Andr\'es} {G\'omez}},
	date-modified = {2021-03-22 15:50:15 +0000},
	note = {Online at \url{https://dialnet.unirioja.es/servlet/articulo?codigo=3216664}},
	pages = {123-140},
	publisher = {University of Rioja},
	title = {Tutorial to {{Locales}} and {{Locale Interpretation}}},
	year = {2010}}


@incollection{keevashCountingSteinerTriple2018,
  title = {Counting {{Steiner Triple Systems}}},
  booktitle = {European {{Congress}} of {{Mathematics}}},
  author = {Keevash, Peter},
  editor = {Mehrmann, Volker and Skutella, Martin},
  year = {2018},
  month = aug,
  pages = {459--481},
  publisher = {{European Mathematical Society Publishing House}},
  address = {{Zuerich, Switzerland}},
  doi = {10.4171/176-1/22},
  abstract = {We prove a conjecture of Wilson from 1974 on the number of Steiner Triple Systems. The proof illustrates our method of Randomised Algebraic Construction, which we developed recently to resolve a question of Steiner from 1853 on the existence of combinatorial designs.},
  file = {C\:\\Users\\cledm\\Zotero\\storage\\MS2LED3K\\Keevash - 2018 - Counting Steiner Triple Systems.pdf},
  isbn = {978-3-03719-176-7},
  language = {en}
}

@article{holzlMarkovChainsMarkov2017,
  title = {Markov {{Chains}} and {{Markov Decision Processes}} in {{Isabelle}}/{{HOL}}},
  author = {H{\"o}lzl, Johannes},
  year = {2017},
  month = oct,
  journal = {Journal of Automated Reasoning},
  volume = {59},
  number = {3},
  pages = {345--387},
  issn = {1573-0670},
  abstract = {This paper presents an extensive formalization of Markov chains (MCs) and Markov decision processes (MDPs), with discrete time and (possibly infinite) discrete state-spaces. The formalization takes a coalgebraic view on the transition systems representing MCs and constructs their trace spaces. On these trace spaces properties like fairness, reachability, and stationary distributions are formalized. Similar to MCs, MDPs are represented as transition systems with a construction for trace spaces. These trace spaces provide maximal and minimal expectation over all possible non-deterministic decisions. As applications we provide a certifier for finite reachability problems and we relate the denotational semantics and operational semantics of the probabilistic guarded command language. A distinctive feature of our formalization is the order-theoretic and coalgebraic view on our concepts: we view transition systems as coalgebras, we view traces as coinductive streams, we provide iterative computation rules for expectations, and we define many properties on traces as least or greatest fixed points.}
}

@inproceedings{BSGPaper,
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},
url = {https://doi.org/10.1145/3573105.3575680},
doi = {10.1145/3573105.3575680},
abstract = {We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemer\'{e}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\'{e}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\'{e}di–Gowers Theorem in any proof assistant to our knowledge.},
booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {225–238},
numpages = {14},
keywords = {Isabelle/HOL, probabilistic method, formalisation of mathematics, interactive theorem proving, additive combinatorics, proof assistant, graph theory},
location = {Boston, MA, USA},
series = {CPP 2023}
}

@book{tao2013introduction,
  title = {An Introduction to Measure Theory},
  author = {Tao, T.},
  year = {2013},
  series = {Graduate Studies in Mathematics},
  publisher = {{American Mathematical Society}},
  url = {https://books.google.co.uk/books?id=SPGJjwEACAAJ},
  isbn = {978-1-4704-0922-7}
}


@inproceedings{noschinskiProofPearl,
  title = {Proof {{Pearl}}: {{A Probabilistic Proof}} for the {{Girth}}-{{Chromatic Number Theorem}}},
  booktitle = {Interactive {{Theorem Proving}}. {{ITP}} 2012.},
  author = {Noschinski, Lars},
  volume = {7406},
  year = {2012},
  editor="Beringer, Lennart
and Felty, Amy",
  publisher = {{Springer, Berlin, Heidelberg}},
  file = {C\:\\Users\\cledm\\Zotero\\storage\\E7ZHIM6P\\978-3-642-32347-8_27.html},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  doi = {https://doi.org/10.1007/978-3-642-32347-8_27}
}


@article{hupelRandomGraphs,
  author  = {Lars Hupel},
  title   = {Properties of Random Graphs -- Subgraph Containment},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Random_Graph_Subgraph_Threshold.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@book{alonProbabilisticMethod2008,
  title = {The Probabilistic Method},
  author = {Alon, Noga and Spencer, Joel H.},
  year = {2016},
  edition = {4th},
  publisher = {{Wiley}},
  address = {{Hoboken, N.J}},
  abstract = {The probabalistic method, allows us to prove the existence of combinatorial structure with certain properties by constructing an appropriate probability space and showing that a chosen element has the desired properties with positive probability},
  file = {C\:\\Users\\cledm\\Zotero\\storage\\WS9HSV4A\\Alon and Spencer - 2008 - The probabilistic method.pdf},
  isbn = {1119061954},
  keywords = {Combinatorial analysis,Probabilities},
  language = {en},
  series = {Wiley-{{Interscience}} Series in Discrete Mathematics and Optimization}
}



@article{bordg2022,
author = {Anthony Bordg and Lawrence C. Paulson and Wenda Li},
title = {Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types},
journal = {Experimental Mathematics},
volume = {31},
number = {2},
pages = {364-382},
year  = {2022},
publisher = {Taylor and Francis},
doi = {10.1080/10586458.2022.2062073},
}

@inproceedings{paulsonThreeYearsExperience2015,
  author    = {Lawrence C. Paulson and Jasmin Christian Blanchette},
  title     = {Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers},
  booktitle = {IWIL 2010. The 8th International Workshop on the Implementation of Logics},
  editor    = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska},
  series    = {EPiC Series in Computing},
  volume    = {2},
  pages     = {1--11},
  year      = {2012},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {https://easychair.org/publications/paper/wV},
  doi       = {10.29007/36dt}}
}


@phdthesis{WenzelIsar2022,
  title = {Isabelle, {{Isar}} - a Versatile Environment for Human Readable Formal Proof Documents},
  author = {Wenzel, Markus},
  year = {2002},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/phd/dnb/Wenzel02a.bib},
  school = {Technical University Munich, Germany},
  timestamp = {Wed, 12 Feb 2020 16:41:48 +0100},
  type = {{{PhD Thesis}}}
}

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