Skip to content

Formalization of Wigderson's graph coloring algorithm in Coq

License

Notifications You must be signed in to change notification settings

siraben/coq-wigderson

Repository files navigation

Towards the Formal Verification of Wigderson’s Algorithm

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.

License

This software is licensed under the MIT license.