← All papers
A verified implementation of the Misra and Gries edge coloring algorithm
cs.DM
Dec 16, 2025 · v1
TL;DR
Uses the Lean theorem prover to build a verified implementation of the Misra-Gries edge-coloring algorithm with maintained invariants.
Abstract
Vizing's theorem states that every simple undirected graph can be edge-colored using fewer than $Δ+ 1$ colors, where $Δ$ 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.
Problem
Vizing's theorem guarantees that every simple undirected graph can be edge-colored using at most Delta+1 colors, but verified implementations of the underlying algorithmic procedure are lacking.
Approach
The author produces a verified implementation of the Misra and Gries edge-coloring algorithm, a modified version of Vizing's original method, using the Lean theorem prover. The work focuses on building libraries for relevant mathematical objects and rigorously maintaining required invariants throughout the algorithm's execution.
Results
The result is a fully verified implementation in Lean that correctly implements the Misra and Gries algorithm, with all required invariants formally maintained and the correctness of the edge coloring proved.