Complexitylib: a blueprint for computational complexity in Lean

1 Introduction

Complexitylib is a Lean 4 formalization of computational complexity theory, built on Mathlib. This blueprint is its map. Each chapter covers one area; each node is a definition or result that is either formalized, with a link to its Lean declaration, or planned, with the results it depends on. The dependency graph shows which planned results are ready to be worked on.

The library’s machine model follows Arora and Barak: multi-tape Turing machines over the alphabet \(\{ 0, 1, \sqcup , \triangleright \} \) with a read-only input tape, work tapes, and an output tape. Complexity classes are defined from this model, so every class-level theorem is a statement about concrete machines. Other models (Boolean circuits, random access machines, interactive protocols, logics) are related to it by explicit simulations.

1.1 Reading the blueprint

  • A node with a Lean link is formalized. Its prose is meant to state the linked Lean statement with all of its hypotheses, but the Lean statement is authoritative: where the two differ, what is proved is the Lean statement. CI checks that every declaration of the library depends on no axioms beyond Lean’s three standard ones, so no declaration uses sorry or a custom axiom. It also checks the blueprint’s links and markers: every Lean name exists; a statement is marked formalized exactly when it has a Lean link; the proof of a linked result is marked formalized; a theorem cites at least one Lean proof, not only definitions; and every label, uses entry, and cross-reference resolves. Nothing checks that the prose matches the Lean statement; that is done by review.

  • A node without a Lean link is planned. Its uses list names the results a proof is expected to need.

  • A result proved under a hypothesis is stated as that implication. For example, the library proves that \(\mathsf{NL} \subseteq \mathsf{coNL}\) implies \(\mathsf{NL} = \mathsf{coNL}\); the unconditional Immerman–Szelepcsényi theorem is a separate planned node. A proved implication never stands in for the theorem it would give.

  • Statements fix their conventions: resource bounds are explicit, encodings are concrete, and malformed inputs are handled. When a textbook result has several variants, the node says which one is formalized.

1.2 How results are proved

Most class-level results in the library are best proved through a small number of characterization theorems rather than by building a new machine:

  • Cobham’s theorem (Theorem 115) makes \(\mathsf{FP}\) a programming language: a function is polynomial-time exactly when it is generated by composition and bounded recursion on notation from a few base functions. Closure lemmas turn this into a toolkit for writing polynomial-time functions as ordinary Lean terms.

  • The witness characterization of \(\mathsf{NP}\): a language with a polynomial-time verifier and polynomially bounded witnesses is in \(\mathsf{NP}\).

  • Iteration in polynomial space: iterating a polynomial-time step function exponentially many times on a polynomial-size state stays in \(\mathsf{PSPACE}\). Savitch’s theorem and \(\mathsf{IP} \subseteq \mathsf{PSPACE}\) are proved this way.

  • Universal simulation (Theorem 30): one fixed machine simulates every machine through the computable compiler \(p \mapsto \langle \alpha , p \rangle \), preserving and reflecting halting and output, with polynomial overhead.

The main gap is logarithmic space, which has no comparable programming layer yet; see the chapter on space complexity.

1.3 Status and priorities

Headline formalized results include Cook–Levin (Theorem 140), Cobham’s theorem, universal simulation, and the deterministic time hierarchy (Theorem 35); each chapter lists the rest. Infrastructure priorities that are not mathematical results, such as proof automation, consolidating duplicated encodings, and CI checks for unproved hypotheses, are described in ROADMAP.md in the repository.