Complexity.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 0 contain sorry, 0 declared as axioms

Complexity Classes

This file contains formal definitions of notions from complexity theory, including the complexity classes P, NP, coNP, and BPP.

References:

Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009.
Melissa Antonelli, Ugo Dal Lago, and Paolo Pistone. On Randomized Computational Models and Complexity Classes: a Historical Overview. 2024. arXiv:2409.11999
Wikipedia: Complexity class

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

abbrev ComplexityTheory.DecisionProblem The type of decision problems line 48 source
Source documentation
The type of decision problems.
We define these as functions from lists of booleans to booleans, implicitly assuming the usual encodings.

no axioms what this means
Proof uses: List, Bool
```
abbrev DecisionProblem := List Bool → Bool
```
abbrev ComplexityTheory.DecisionComplexityClass The type of complexity classes line 53 source
Source documentation
The type of complexity classes. We define these as sets of decision problems.

no axioms what this means
Proof uses: Set, ComplexityTheory.DecisionProblem
```
abbrev DecisionComplexityClass := Set DecisionProblem
```
Mentions: ComplexityTheory.DecisionProblem
def ComplexityTheory.IsPolyTimeWithEncoding IsPolyTimeWithEncoding ea eb f asserts that f is computable in polynomial time when its input and output are encoded via the given Encodings ea and eb line 59 source
Source documentation
IsPolyTimeWithEncoding ea eb f asserts that f is computable in polynomial time when its input and output are encoded via the given Encodings ea and eb.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Computability.Encoding
Proof uses: Nonempty, Turing.TM2ComputableInPolyTime, Computability.Encoding.encode
```
def IsPolyTimeWithEncoding {α β Γα Γβ : Type} (ea : Encoding α Γα) (eb : Encoding β Γβ)
    (f : α → β) :=
…
```
def ComplexityTheory.IsPolyTime Documented declaration: IsPolyTime line 68 source
Source documentation
A function is polynomial-time computable when it is IsPolyTimeWithEncoding for the canonical Bool-alphabet encodings of its domain and codomain as given by the BitstringEncoding typeclass.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: BitstringEncoding
Proof uses: ComplexityTheory.IsPolyTimeWithEncoding, Bool, BitstringEncoding.toEncoding
```
def IsPolyTime {α β : Type} [BitstringEncoding α] [BitstringEncoding β] (f : α → β) : Prop :=
…
```
Mentions: BitstringEncoding
theorem ComplexityTheory.isPolyTime_id The identity function is polynomial-time computable line 72 source
Source documentation
The identity function is polynomial-time computable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: BitstringEncoding, ComplexityTheory.IsPolyTime, id
Proof uses: Nonempty.intro, Turing.TM2ComputableInPolyTime, Bool, Computability.Encoding.encode, BitstringEncoding.toEncoding, Turing.idComputableInPolyTime, BitstringEncoding.bitEncode
1 instances, coercions and auxiliary constants left out.
```
theorem isPolyTime_id {α : Type} [BitstringEncoding α] : IsPolyTime (id : α → α) :=
…
```
Mentions: BitstringEncoding, ComplexityTheory.IsPolyTime
def ComplexityTheory.P The class P is the set of decision problems decidable in polynomial time by a deterministic Turing machine line 81 source
Source documentation
The class P is the set of decision problems decidable in polynomial time by a deterministic Turing machine.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ComplexityTheory.DecisionComplexityClass
Proof uses: Set.ofPred, ComplexityTheory.DecisionProblem, ComplexityTheory.IsPolyTime, List, Bool
2 instances, coercions and auxiliary constants left out.
```
def P : DecisionComplexityClass :=
…
```
Mentions: ComplexityTheory.DecisionComplexityClass
def ComplexityTheory.NP The class NP is the set of decision problems line 93 source
Source documentation
The class NP is the set of decision problems $L$ such that there exists a polynomial $p$ over ℕ and a poly-time Turing machine computing a relation $R$ where for all $x$, $L(x)$ iff there exists a $w$ of length at most $p (|x|)$ such that $R(x,w)$ accepts.
See Definition 2.1 in Arora-Barak (2009).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ComplexityTheory.DecisionComplexityClass
Proof uses: Set.ofPred, ComplexityTheory.DecisionProblem, Exists, Polynomial, Nat, Prod, List, Bool, And, ComplexityTheory.IsPolyTime, Iff, Eq, Bool.true, LE.le, List.length, Polynomial.eval, Prod.mk
5 instances, coercions and auxiliary constants left out.
```
def NP : DecisionComplexityClass :=
…
```
Mentions: ComplexityTheory.DecisionComplexityClass
def ComplexityTheory.coNP The class coNP is the set of decision problems whose complements are in NP line 102 source
Source documentation
The class coNP is the set of decision problems whose complements are in NP.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ComplexityTheory.DecisionComplexityClass
Proof uses: Set.ofPred, ComplexityTheory.DecisionProblem, Membership.mem, ComplexityTheory.NP, Compl.compl, List, Bool
4 instances, coercions and auxiliary constants left out.
```
def coNP : DecisionComplexityClass :=
…
```
Mentions: ComplexityTheory.DecisionComplexityClass
def ComplexityTheory.BPP The class BPP is the set of decision problems line 114 source
Source documentation
The class BPP is the set of decision problems $L$ such that there exists a polynomial $p$ over ℕ and a poly-time Turing machine computing a relation $R$ where for all $x$, a uniformly random string $r$ of length $p (|x|)$ satisfies $R (x, r) = L (x)$ with probability at least $2/3$.
See Definition 7.4 in Arora-Barak (2009), or Antonelli et al. (2024).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ComplexityTheory.DecisionComplexityClass
Proof uses: Set.ofPred, ComplexityTheory.DecisionProblem, Exists, Polynomial, Nat, Prod, List, Bool, And, ComplexityTheory.IsPolyTime, LE.le, Rat, HDiv.hDiv, OfNat.ofNat, Finset.card, Fin, Polynomial.eval, List.length, Finset.filter, Eq and 4 more
17 instances, coercions and auxiliary constants left out.
```
def BPP : DecisionComplexityClass :=
…
```
Mentions: ComplexityTheory.DecisionComplexityClass