Vision
AlgoLib aims to formalize algorithms and the theory they rest on,
with proofs of both correctness and runtime, in a way
that stays close to the informal definitions used across
the standard 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 before moving on to more advanced material. The three groups below
mirror the top-level structure of the library: Theory/,
Algorithms/, and DataStructures/.
Theory
- Walks & connectivitywalks, paths, cycles, Eulerian walks, components
- Treestrees and forests, Cayley's theorem
- SpectralLaplacian, Cheeger's inequality, expanders
- Matchingsaugmenting paths, Hall's theorem, König's theorem
- Coloringsproper vertex and edge colorings, chromatic bounds
- Minorscontractions, minors, topological minors
- PlanarityEuler's formula, Kuratowski, toroidal graphs
Algorithms
- FlowsFord–Fulkerson, Edmonds–Karp, Push–Relabel
- TraversalBFS, DFS
- Shortest pathsDijkstra, Bellman–Ford, Floyd–Warshall
- Spanning treesKruskal, Prim, Borůvka
- SCCTarjan, Kosaraju
Data structures
- Union–Findunion-by-rank with path compression
- Binary search treesordered maps and sets over a BST API
- Splay treesamortised bounds, sequential access theorem