Wood, PhilipAmin, NadaGrinstead, Kathleen Milligan2026-07-0720262026-06-022026Grinstead, Kathleen Milligan. 2026. Vizing's Theorem in Rocq. Bachelors Thesis, Harvard University Engineering and Applied Sciences.32575818https://dash.harvard.edu/handle/1/42743944This 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.application/pdfenEdge coloringGraph theoryProof assistantsRocqComputer scienceMathematicsThesis or Dissertation2026-07-070009-0006-8162-4633