1
Introduction
▶
1.1
Reading the blueprint
1.2
How results are proved
1.3
Status and priorities
2
Machine models
▶
2.1
Turing machines
2.2
Output semantics
2.3
Combinators and Hoare-style specifications
2.4
Reduction to one work tape
2.5
Universal simulation
2.6
The time hierarchy
2.7
Random access machines
2.8
Finite automata and one-way liveness
▶
2.8.1
Nondeterministic complementation
3
Encodings and finite probability
▶
3.1
Bit strings
3.2
Self-delimiting blocks and pairing
3.3
Other formalized codes
3.4
A reusable codec interface
3.5
Finite counting
3.6
Event probability
3.7
Repetition of probabilistic machines
3.8
Zero-error randomized computation
4
Polynomial time, reductions, and NP
▶
4.1
Time classes
4.2
Closure properties of P and FP
4.3
Cobham’s theorem: FP as a programming language
4.4
Witnesses, FNP, and TFNP
4.5
Reductions and completeness
4.6
Satisfiability and the Cook–Levin theorem
4.7
More NP-complete problems
4.8
Noncommutative rational hitting lists
4.9
Open directions
5
Randomness, counting, and the polynomial hierarchy
▶
5.1
Randomized classes
5.2
The polynomial hierarchy
5.3
The Sipser–Lautemann theorem
5.4
Counting classes
5.5
Polynomial-space upper bounds
5.6
Hashing and approximate counting
6
Space, alternation, and QBF
▶
6.1
Space-bounded deciders and classes
6.2
Elementary containments and closure
6.3
Configuration graphs and space-to-time
6.4
Nondeterministic logarithmic space
6.5
Savitch’s theorem and the iteration lever
6.6
Quantified Boolean formulas and alternation
6.7
Space hierarchy
6.8
A log-space programming layer
7
Circuits, advice, and uniformity
▶
7.1
The circuit model
7.2
Wire uses and shared gates
7.3
Circuit families and \(\mathsf{P/poly}\)
7.4
Circuit cuts
7.5
Advice
7.6
Serialized circuits and their evaluation
7.7
Functional unrolling
7.8
Logspace uniformity
7.9
\(\mathsf{BPP}\) is contained in \(\mathsf{P/poly}\)
7.10
Small-depth classes
7.11
Shallow circuits for symmetric functions
7.12
Formulas and Barrington’s theorem
7.13
Open directions
7.14
Unrestricted depth-three circuits beyond the square-root exponent
7.15
Exact scalar Fourier circuits
8
Circuit lower bounds and proof complexity
▶
8.1
Counting bounds
8.2
Results from the algebraic-circuits library
▶
Sparse corrections in CSLib’s circuit model.
8.3
The frontier method
▶
8.3.1
Exponentially small correlation
8.4
Essential inputs and gate elimination
8.5
Depth, formulas, and communication
8.6
Restrictions, normal forms, and decision trees
8.7
The switching lemma and \(\mathsf{AC}^0\)
▶
8.7.1
Depth-three circuits and subcube dispersers
8.8
Threshold circuits of unbounded depth
8.9
Polynomial approximation and \(\mathsf{AC}^0[3]\)
8.10
Monotone circuits
8.11
Proof complexity
8.12
Top-down parity and majority lower bounds
▶
8.12.1
Majority extension
9
Interactive proofs and PCPs
▶
9.1
Interactive protocols
9.2
Algebraic tools and IP = PSPACE
9.3
Probabilistically checkable proofs
9.4
Hardness of approximation
10
Relativization and natural proofs
▶
10.1
Oracle machines
10.2
Relativized classes and the Baker–Gill–Solovay worlds
10.3
Natural proofs
11
Metacomplexity
▶
11.1
Promise problems
11.2
Machine-relative Kolmogorov complexity
11.3
Minimum time-bounded Kolmogorov complexity
11.4
The minimum circuit size problem
11.5
Anti-checkers and hardness magnification
11.6
Codes
12
Average-case complexity and the Hirahara program
▶
12.1
Ensembles and errorless heuristics
12.2
MINKT under the auxiliary-unary distribution
12.3
Nisan–Wigderson reconstruction
12.4
Conditional complexity, depth, and symmetry of information
12.5
Gap problems and the conditional collapse
12.6
Further theorems of the program
12.7
Open directions
13
Analysis of Boolean functions
▶
Conventions.
13.1
The cube and the Fourier basis
13.2
Degree structure
13.3
Linearity testing
13.4
Noise
13.5
Influence and derivatives
13.6
Monotone functions
13.7
Hypercontractivity
13.8
Consequences of hypercontractivity
13.9
Fourier concentration of constant-depth circuits
13.10
Exponential correlation bounds for binary polynomials
13.11
Harmonic means and top-down lower bounds
13.12
Polynomial threshold functions and the Gotsman–Linial bound
13.13
Correlation and threshold weight
13.14
Sensitivity and exact query complexity
14
Descriptive complexity
▶
Conventions.
14.1
Vocabularies and finite structures
14.2
First-order logic
14.3
Boolean queries and definability
14.4
Second-order logic
14.5
Encodings and model checking
14.6
First-order reductions
14.7
Capturing complexity classes
14.8
Open directions
15
Frontiers: directions beyond the current tracks
▶
15.1
Hardness of approximation
15.2
Derandomization
15.3
Space-bounded derandomization
15.4
Cryptographic foundations
15.5
Communication complexity
15.6
Algebraic complexity
15.7
Fine-grained and parameterized complexity
15.8
Quantum computation
Dependency graph
Complexitylib: a blueprint for computational complexity in Lean
The Complexitylib contributors
1
Introduction
1.1
Reading the blueprint
1.2
How results are proved
1.3
Status and priorities
2
Machine models
2.1
Turing machines
2.2
Output semantics
2.3
Combinators and Hoare-style specifications
2.4
Reduction to one work tape
2.5
Universal simulation
2.6
The time hierarchy
2.7
Random access machines
2.8
Finite automata and one-way liveness
2.8.1
Nondeterministic complementation
3
Encodings and finite probability
3.1
Bit strings
3.2
Self-delimiting blocks and pairing
3.3
Other formalized codes
3.4
A reusable codec interface
3.5
Finite counting
3.6
Event probability
3.7
Repetition of probabilistic machines
3.8
Zero-error randomized computation
4
Polynomial time, reductions, and NP
4.1
Time classes
4.2
Closure properties of P and FP
4.3
Cobham’s theorem: FP as a programming language
4.4
Witnesses, FNP, and TFNP
4.5
Reductions and completeness
4.6
Satisfiability and the Cook–Levin theorem
4.7
More NP-complete problems
4.8
Noncommutative rational hitting lists
4.9
Open directions
5
Randomness, counting, and the polynomial hierarchy
5.1
Randomized classes
5.2
The polynomial hierarchy
5.3
The Sipser–Lautemann theorem
5.4
Counting classes
5.5
Polynomial-space upper bounds
5.6
Hashing and approximate counting
6
Space, alternation, and QBF
6.1
Space-bounded deciders and classes
6.2
Elementary containments and closure
6.3
Configuration graphs and space-to-time
6.4
Nondeterministic logarithmic space
6.5
Savitch’s theorem and the iteration lever
6.6
Quantified Boolean formulas and alternation
6.7
Space hierarchy
6.8
A log-space programming layer
7
Circuits, advice, and uniformity
7.1
The circuit model
7.2
Wire uses and shared gates
7.3
Circuit families and \(\mathsf{P/poly}\)
7.4
Circuit cuts
7.5
Advice
7.6
Serialized circuits and their evaluation
7.7
Functional unrolling
7.8
Logspace uniformity
7.9
\(\mathsf{BPP}\) is contained in \(\mathsf{P/poly}\)
7.10
Small-depth classes
7.11
Shallow circuits for symmetric functions
7.12
Formulas and Barrington’s theorem
7.13
Open directions
7.14
Unrestricted depth-three circuits beyond the square-root exponent
7.15
Exact scalar Fourier circuits
8
Circuit lower bounds and proof complexity
8.1
Counting bounds
8.2
Results from the algebraic-circuits library
Sparse corrections in CSLib’s circuit model.
8.3
The frontier method
8.3.1
Exponentially small correlation
8.4
Essential inputs and gate elimination
8.5
Depth, formulas, and communication
8.6
Restrictions, normal forms, and decision trees
8.7
The switching lemma and \(\mathsf{AC}^0\)
8.7.1
Depth-three circuits and subcube dispersers
8.8
Threshold circuits of unbounded depth
8.9
Polynomial approximation and \(\mathsf{AC}^0[3]\)
8.10
Monotone circuits
8.11
Proof complexity
8.12
Top-down parity and majority lower bounds
8.12.1
Majority extension
9
Interactive proofs and PCPs
9.1
Interactive protocols
9.2
Algebraic tools and IP = PSPACE
9.3
Probabilistically checkable proofs
9.4
Hardness of approximation
10
Relativization and natural proofs
10.1
Oracle machines
10.2
Relativized classes and the Baker–Gill–Solovay worlds
10.3
Natural proofs
11
Metacomplexity
11.1
Promise problems
11.2
Machine-relative Kolmogorov complexity
11.3
Minimum time-bounded Kolmogorov complexity
11.4
The minimum circuit size problem
11.5
Anti-checkers and hardness magnification
11.6
Codes
12
Average-case complexity and the Hirahara program
12.1
Ensembles and errorless heuristics
12.2
MINKT under the auxiliary-unary distribution
12.3
Nisan–Wigderson reconstruction
12.4
Conditional complexity, depth, and symmetry of information
12.5
Gap problems and the conditional collapse
12.6
Further theorems of the program
12.7
Open directions
13
Analysis of Boolean functions
Conventions.
13.1
The cube and the Fourier basis
13.2
Degree structure
13.3
Linearity testing
13.4
Noise
13.5
Influence and derivatives
13.6
Monotone functions
13.7
Hypercontractivity
13.8
Consequences of hypercontractivity
13.9
Fourier concentration of constant-depth circuits
13.10
Exponential correlation bounds for binary polynomials
13.11
Harmonic means and top-down lower bounds
13.12
Polynomial threshold functions and the Gotsman–Linial bound
13.13
Correlation and threshold weight
13.14
Sensitivity and exact query complexity
14
Descriptive complexity
Conventions.
14.1
Vocabularies and finite structures
14.2
First-order logic
14.3
Boolean queries and definability
14.4
Second-order logic
14.5
Encodings and model checking
14.6
First-order reductions
14.7
Capturing complexity classes
14.8
Open directions
15
Frontiers: directions beyond the current tracks
15.1
Hardness of approximation
15.2
Derandomization
15.3
Space-bounded derandomization
15.4
Cryptographic foundations
15.5
Communication complexity
15.6
Algebraic complexity
15.7
Fine-grained and parameterized complexity
15.8
Quantum computation