Tue 21 Jan 2020 15:56 - 16:18 at Maurepas - Formalized mathematics 1 Chair(s): Robert Y. Lewis

The Perfect Graph Theorems are important results in graph theory describing the relationship between clique number $\omega(G)$ and chromatic number $\chi(G)$ of a graph $G$. A graph $G$ is called \emph{perfect} if $\chi(H)=\omega(H)$ for every induced subgraph $H$ of $G$. The Strong Perfect Graph Theorem (SPGT) states that a graph is perfect if and only if it does not contain an odd hole (or an odd anti-hole) as its induced subgraph. The Weak Perfect Graph Theorem (WPGT) states that a graph is perfect if and only if its complement is perfect. In this paper, we present a formal framework for working with finite simple graphs. We model finite simple graphs in the Coq Proof Assistant by representing its vertices as a finite set over a countably infinite domain. We argue that this approach provides a formal framework in which it is convenient to work with different types of graph constructions (or expansions) involved in the proof of the Lov'{a}sz Replication Lemma (LRL), which is also the key result used in the proof of Weak Perfect Graph Theorem. Finally, we use this setting to develop a constructive formalization of the Weak Perfect Graph Theorem.

 Slides (cpp_ppt.pdf) 401KiB

#### Tue 21 JanDisplayed time zone: Saskatchewan, Central America change

 15:35 - 16:40 Formalized mathematics 1CPP at Maurepas Chair(s): Robert Y. Lewis Vrije Universiteit Amsterdam 15:3521mTalk Formalising perfectoid spacesCPPPatrick Massot Université Paris Sud, Kevin Buzzard Imperial College London, Johan Commelin Universität Freiburg DOI Pre-print Media Attached File Attached 15:5621mTalk A Constructive Formalization of the Weak Perfect Graph TheoremCPPAbhishek Kr Singh Tata Institute of Fundamental Research Mumbai, Raja Natarajan Tata Institute of Fundamental Research Mumbai DOI Pre-print Media Attached File Attached 16:1821mTalk Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in CoqCPPChristian Doczkal Université Côte d'Azur, Damien Pous CNRS, ENS Lyon DOI Pre-print Media Attached