A verified implementation of the Misra and Gries edge coloring algorithm

TL;DR

This paper presents a formally verified implementation of the Misra and Gries edge coloring algorithm in the Lean theorem prover, ensuring correctness for graph coloring based on Vizing's theorem.

Contribution

It provides the first verified implementation of the Misra and Gries algorithm, with rigorous formalization and invariant maintenance in Lean.

Findings

Verified correctness of the edge coloring algorithm

Built comprehensive libraries for graph theory in Lean

Ensured invariants are maintained throughout the implementation

Abstract

Vizing's theorem states that every simple undirected graph can be edge-colored using fewer than $\Delta + 1$ colors, where $\Delta$ is the graph's maximum degree. The original proof was given through a polynomial-time algorithmic procedure that iteratively extends a partial coloring until it becomes complete. In this work, I used the Lean theorem prover to produce a verified implementation of the Misra and Gries edge-coloring algorithm, a modified version of Vizing's original method. The focus is on building libraries for relevant mathematical objects and rigorously maintaining required invariants.