Formalization of algorithmic graph theory in Lean 4

A library of machine-checked definitions, theorems, and algorithms for graphs, covering the standard undergraduate-through-graduate curriculum. It spans walks, trees, and colorings through spectral methods, matchings, and planarity, alongside classical algorithms shipped with proofs of correctness and runtime.

View on GitHub Documentation Blueprint Paper Vision
×

Vision

GraphLib aims to formalize graph theory and its algorithms, with proofs of both correctness and runtime, in a way that stays close to the informal definitions used across the standard graph theory literature. The intent is to minimize the overhead for practitioners coming from textbook mathematics, so that statements, objects, and arguments in Lean read as directly as possible like their pen-and-paper counterparts.

Where definitions and results prove generally useful, the long-term goal is to upstream contributions back to Mathlib and cslib, so that the broader Lean ecosystem benefits.

Roadmap

For v1, we aim to formalize the following fundamental concepts in graph theory before moving on to more advanced definitions.

Theory

Algorithms