# Towards a constructive formalization of Perfect Graph Theorems

## TL;DR

This paper develops a formal framework in Coq to verify key theorems in perfect graph theory, including a constructive proof of the Lovász Replication Lemma, enhancing rigor and formal understanding.

## Contribution

It introduces a constructive formalization of perfect graph theorems in Coq, providing a verified proof of the Lovász Replication Lemma without additional axioms.

## Key findings

- Formal framework for perfect graph theorems in Coq
- Constructive proof of Lovász Replication Lemma
- Verification of Strong and Weak Perfect Graph Theorems

## Abstract

Interaction between clique number $\omega(G) $ and chromatic number $\chi(G) $ of a graph is a well studied topic in graph theory. Perfect Graph Theorems are probably the most important results in this direction. 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 verifying these results. We model finite simple graphs in the constructive type theory of Coq Proof Assistant without adding any axiom to it. Finally, we use this framework to present a constructive proof of the Lov\'{a}sz Replication Lemma, which is the central idea in the proof of Weak Perfect Graph Theorem.