A Guide to cslib-frontier🔗

cslib-frontier is the frontier formalization library for CSLib, built on CSLib and Mathlib; its scope is computer science generally, from algorithms and data structures to complexity, cryptography and logic. 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 results inventory collects named results with their theorem names and sources.

• ROADMAP.md records outstanding work, and CONTRIBUTING.md explains how to propose and review changes.

The guide is new: after first steps, it has chapters on NP-completeness, unweighted graph matching, streaming, and first-order logic with operators. Further areas follow one at a time, and each chapter's friction points are fixed in the library rather than documented around.