Created by: Ben Siraphob (siraben) and Jamison Homatas (jhomatas48)
We present progress towards the formal verification of Wigderson's graph coloring algorithm in Coq. We have created a library of formalized graph theory that aims to bridge the literature gap between introductory material on Coq and large-scale formal developments, while providing a motivating case study. Our library contains over 180 proven theorems.
Using Nix, run nix-shell
then run make
to compile it.
This software is licensed under the MIT license.