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
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
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
Circuit families and \(\mathsf{P/poly}\)
7.3
Advice
7.4
Serialized circuits and their evaluation
7.5
Functional unrolling
7.6
Logspace uniformity
7.7
\(\mathsf{BPP}\) is contained in \(\mathsf{P/poly}\)
7.8
Small-depth classes
7.9
Formulas and Barrington’s theorem
7.10
Open directions
8
Circuit lower bounds and proof complexity
▶
8.1
Counting bounds
8.2
Results from the algebraic-circuits library
8.3
Essential inputs and gate elimination
8.4
Depth, formulas, and communication
8.5
Restrictions, normal forms, and decision trees
8.6
The switching lemma and \(\mathsf{AC}^0\)
8.7
Monotone circuits
8.8
Proof complexity
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
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
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
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
Circuit families and \(\mathsf{P/poly}\)
7.3
Advice
7.4
Serialized circuits and their evaluation
7.5
Functional unrolling
7.6
Logspace uniformity
7.7
\(\mathsf{BPP}\) is contained in \(\mathsf{P/poly}\)
7.8
Small-depth classes
7.9
Formulas and Barrington’s theorem
7.10
Open directions
8
Circuit lower bounds and proof complexity
8.1
Counting bounds
8.2
Results from the algebraic-circuits library
8.3
Essential inputs and gate elimination
8.4
Depth, formulas, and communication
8.5
Restrictions, normal forms, and decision trees
8.6
The switching lemma and \(\mathsf{AC}^0\)
8.7
Monotone circuits
8.8
Proof complexity
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
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