Complexitylib

Complexitylib is a Lean 4 library of computational complexity theory, built on CSLib and Mathlib. It develops reusable arguments about algorithms, resource bounds, reductions, lower bounds, and cryptographic security.

A central goal is to let you write recognizable functional programs and prove their efficiency compositionally, with Turing-machine implementations justified underneath. Nonconstructive mathematics and model-specific lower bounds also belong. Developments should establish useful results or make those results easier to state, prove, and reuse.

Development is AI-assisted. Contributors are responsible for the mathematical statements, source attribution, and maintainability of their changes. Lean checks proofs against their stated definitions; independent review checks that those definitions and statements express the intended mathematics. See Contributing to propose, implement, or review a development.

Start here

I want to…	Start with…
Certify functional programs and loops	PolyTime examples
Construct circuits for polynomial-time function families	Uniform circuit examples
Write probabilistic programs or oracle reductions	PPT examples, oracle examples
Find a computational model or mathematical tool	Module index; each module documents its definitions, results, and references
Contribute a result or improve an API	Contributing

The checked examples show fun_prop, polytime, and ppt with explicit encodings and client-supplied invariants. The deterministic backend builds on Christian Reitwiessner's tidy machine calculus.

The theorem index gives selected proved statements with their assumptions, formalization scope and links to Lean declarations. Its LaTeX source and editing guide are maintained alongside the library; it is a curated catalogue, not an exhaustive API reference.

Selected developments

• Cook–Levin: SAT NP-completeness and UNSAT coNP-completeness, including the polynomial-time tableau reduction.
• Structural complexity: Ladner's theorem, a Baker–Gill–Solovay oracle with P^A ≠ NP^A, a time hierarchy with a polynomial gap for bit-string problems and P ⊊ EXP, NPSPACE = PSPACE, TQBF PSPACE-completeness, NL ⊆ P, USTCON ∈ L, Toda's theorem PH ⊆ P^#P, Sipser–Gács–Lautemann, BPP ⊆ P/poly and worst-case-hardness derandomization.
• Interactive proofs: NP ⊆ IP, Shamir's theorem IP = PSPACE, and private- and public-coin protocols for graph non-isomorphism (in AM).
• NP-completeness of 3-coloring, Hamiltonian cycle, TSP, subset sum and further graph and number problems, by polynomial-time reductions.
• Total search: LocalOpt, Pigeon, EndOfLine and Leaf are complete for PLS, PPP, PPAD and PPA, using polynomial-time construction of their circuit codes.
• Fagin's theorem: a class of finite relational structures is definable in existential second-order logic exactly when it is closed under isomorphism and in NP.
• One-way functions to PRGs and adaptive PRFs, including Goldreich–Levin, polynomial stretch, and GGM, with efficient security reductions.
• Circuit APIs: Boolean, monotone, and arithmetic developments share CSLib's circuit definitions, costs, and simulations. The quadratic-form correlation bound uses a nonconstructively chosen family; it supplies no efficient construction.
• The PCP theorem: NP = PCP(log n, 1), with polynomial-time construction and verification, perfect completeness and soundness at most one half. The proof uses Dinur's gap construction and the library's deterministic-verifier definition of NP. Expander rotations are polynomial in the vertex count; the fixed construction constants remain enormous.

Build and use

The package is named complexitylib; imports begin with Complexity.. Most declaration namespaces begin with Cslib, and Turing-machine declarations use Turing. Use the version in lean-toolchain and the pinned dependencies in lakefile.toml. From a checkout:

lake exe cache get
lake build --wfail --iofail

Import the specific modules you need. import Complexity imports the whole library.

To build searchable API documentation from the module docstrings (Python 3.11+):

python3 scripts/check_docs.py --config-only
lake -d docbuild build Complexity:docs
python3 scripts/check_docs.py
python3 -m http.server --bind 127.0.0.1 --directory docbuild/.lake/build/doc

Open http://localhost:8000 to browse and search. The on-demand API documentation workflow also produces an api-docs artifact; serve it by replacing the directory argument above with the extracted artifact directory.

This is the canonical CSLib-based Complexitylib. The renamed historical pre-CSLib implementation remains available with archival pending; it has a different API, and some developments remain to be ported. The temporary repository and package name complexitylib2 was retired when this repository moved to CSLib Community. Downstream projects using that package name should change it to complexitylib; Lean imports remain unchanged. APIs are still evolving, so downstream projects should pin a commit.

Project information

Modules follow CSLib's APIs, paths, namespaces, and contribution standards so they can move upstream with the import prefix changed from Complexity. to Cslib.. Acceptance requires CSLib review. ROADMAP.md records outstanding work; UPSTREAM.md records upstream coordination and exceptional integration decisions.

Source headers retain authorship, module docstrings credit mathematical and formalization sources, and references.bib contains the bibliography. Licensed under Apache 2.0.