Vizing's Theorem in Rocq

Abstract

This thesis explores Vizing's theorem in the proof assistant Rocq. We employ the SSReflect language and the open-source Mathematical Components library to extend the graph theory library developed by Christian Doczkal, Damien Pous, and Daniel Severín. Specifically, we implement edge coloring and a proof of Vizing's theorem in Rocq. The corresponding code can be viewed in the appendix or at https://github.com/milligang/vizing-thesis. We create the necessary data structures and types to support the proof, and we discuss the representations chosen. In addition, we present a detailed written mathematical proof of the theorem which the formalized Rocq proof follows.