A Guide to Complexitylib
Complexitylib is a Lean 4 library of computational complexity theory, built on CSLib and Mathlib. This guide introduces the library one area at a time, in the order a newcomer needs it: what the objects are, how to state an ordinary claim, and how to prove one. Every Lean example is elaborated against the library when the guide is built, so an example that no longer matches the library fails the build.
Names in the examples link to the API documentation, which lists every declaration with its docstring and source. Other entry points:
The README's Start here table points to checked examples for each kind of task.
The selected formal abstracts state the library's headline results with every definition they use, also as PDFs.
ROADMAP.md records outstanding work, and CONTRIBUTING.md explains how to propose and review changes.
The guide is new: after first steps, it has a chapter on NP-completeness. Further areas follow one at a time, and each chapter's friction points are fixed in the library rather than documented around.