diff --git a/Complexity/Computability/Communication/Protocol.lean b/Complexity/Computability/Communication/Protocol.lean
index beefcf4f7..f15bc38af 100644
--- a/Complexity/Computability/Communication/Protocol.lean
+++ b/Complexity/Computability/Communication/Protocol.lean
@@ -189,6 +189,8 @@ theorem exists_solves_depth_eq_ecomplexity (h : ∃ p : Protocol X Y Z, p.Solves
     (fun p : {p : Protocol X Y Z // p.Solves R A B} => (p.1.depth : ℕ∞))
   exact ⟨p, hp, hmin⟩
 
+/-- Upper bounds on communication complexity: `R` has communication complexity at most `k` on
+`A × B` exactly when some protocol of depth at most `k` solves it. -/
 theorem ecomplexity_le_iff {k : ℕ} :
     ecomplexity R A B ≤ k ↔ ∃ p : Protocol X Y Z, p.Solves R A B ∧ p.depth ≤ k := by
   constructor
@@ -228,10 +230,14 @@ theorem solves_univ_iff : p.Solves (fun x y z => f x y = z) Set.univ Set.univ 
 theorem ecomplexityFun_le_depth (hp : p.run = f) : ecomplexityFun f ≤ p.depth :=
   ecomplexity_le_depth (solves_univ_iff.mpr hp)
 
+/-- Computing `f` has communication complexity at most `k` exactly when some protocol of depth at
+most `k` computes `f`. -/
 theorem ecomplexityFun_le_iff {k : ℕ} :
     ecomplexityFun f ≤ k ↔ ∃ p : Protocol X Y Z, p.run = f ∧ p.depth ≤ k := by
   simp only [ecomplexityFun, ecomplexity_le_iff, solves_univ_iff]
 
+/-- Lower bounds on the communication complexity of `f` are lower bounds on the depth of every
+protocol computing `f`, including when there is none. -/
 theorem le_ecomplexityFun_iff {k : ℕ∞} :
     k ≤ ecomplexityFun f ↔ ∀ p : Protocol X Y Z, p.run = f → k ≤ p.depth := by
   simp only [ecomplexityFun, le_ecomplexity_iff, solves_univ_iff]
diff --git a/Complexity/Computability/Communication/RoundProtocol.lean b/Complexity/Computability/Communication/RoundProtocol.lean
index 8805b6c53..aa65b251d 100644
--- a/Complexity/Computability/Communication/RoundProtocol.lean
+++ b/Complexity/Computability/Communication/RoundProtocol.lean
@@ -154,6 +154,8 @@ def comap (φ : X' → X) (ψ : Y' → Y) :
   | _, .alice send next => .alice (send ∘ φ) fun a => (next a).comap φ ψ
   | _, .bob send next => .bob (send ∘ ψ) fun a => (next a).comap φ ψ
 
+/-- Relabelling the inputs is precomposition: `P.comap φ ψ` outputs on `x` and `y` what `P` outputs
+on `φ x` and `ψ y`. -/
 @[simp] theorem run_comap (φ : X' → X) (ψ : Y' → Y) : ∀ {d : ℕ} (P : RoundProtocol X Y M Z d)
     (x : X') (y : Y'), (P.comap φ ψ).run x y = P.run (φ x) (ψ y)
   | _, .output _, _, _ => rfl
@@ -178,6 +180,8 @@ def ofProtocol : (p : Protocol X Y Z) → (d : ℕ) → p.depth ≤ d → RoundP
     cond b (ofProtocol p₁ d (le_of_max_le_right (Nat.le_of_succ_le_succ h)))
       (ofProtocol p₀ d (le_of_max_le_left (Nat.le_of_succ_le_succ h)))
 
+/-- A bit protocol of depth at most `d`, run as a round protocol with `d` messages, has the same
+output. -/
 @[simp] theorem run_ofProtocol : ∀ (p : Protocol X Y Z) (d : ℕ) (h : p.depth ≤ d) (x : X) (y : Y),
     (ofProtocol p d h).run x y = p.run x y
   | .output _, _, _, _, _ => rfl
diff --git a/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean b/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
index ac199424c..7e6071185 100644
--- a/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
+++ b/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
@@ -293,6 +293,8 @@ private theorem mk_polyOfBits_one (l : List Bool) :
   · rw [List.length_append, List.length_singleton, List.length_concat, List.take_succ_cons]
     simp [bitEquiv_symm_true]
 
+/-- For a coefficient list `g = l ++ [true]` with top coefficient one, `modBits g f` is congruent
+to `f` modulo the polynomial of `g`: both have the same image in `AdjoinRoot (polyOfBits g)`. -/
 theorem mk_polyOfBits_modBits (l f : List Bool) :
     AdjoinRoot.mk (polyOfBits (l ++ [true])) (polyOfBits (modBits (l ++ [true]) f)) =
       AdjoinRoot.mk (polyOfBits (l ++ [true])) (polyOfBits f) := by
@@ -354,6 +356,8 @@ def isIrreducibleCode (m : ℕ) : Bool :=
   decide (2 ≤ m) && (List.range m).all fun d =>
     decide (d < 2) || decide (Nat.log 2 m / 2 < Nat.log 2 d) || (modBits d.bits m.bits).any id
 
+/-- **Trial division decides irreducibility**: `isIrreducibleCode m` holds exactly when the binary
+polynomial with code `m` is irreducible. -/
 theorem isIrreducibleCode_iff (m : ℕ) :
     isIrreducibleCode m = true ↔ Irreducible (polyOfCode m) := by
   unfold isIrreducibleCode
diff --git a/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean b/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
index 962524b7d..47a61f503 100644
--- a/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
+++ b/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
@@ -127,6 +127,8 @@ product `B u * B w`. -/
 def IsMulTable (B : Basis (Fin n) (ZMod 2) F) (tab : List (List (List Bool))) : Prop :=
   tab.length = n ∧ ∀ u w : Fin n, B u * B w = fieldOfBits B (tableEntry tab u w)
 
+/-- With a multiplication table of the basis `B`, `fieldMul` multiplies: the element with
+coordinates `fieldMul tab a b` is the product of those with coordinates `a` and `b`. -/
 theorem fieldOfBits_fieldMul {B : Basis (Fin n) (ZMod 2) F} {tab : List (List (List Bool))}
     (htab : IsMulTable B tab) (a b : List Bool) :
     fieldOfBits B (fieldMul tab a b) = fieldOfBits B a * fieldOfBits B b := by
@@ -229,6 +231,9 @@ private theorem fieldOfBits_foldl_esymmStep {B : Basis (Fin n) (ZMod 2) F}
     rw [List.foldl_cons, h2 j (by rw [hlen]; exact hj), List.map_cons, ← Multiset.cons_coe,
       Multiset.cons_add, Multiset.add_cons]
 
+/-- **The dynamic program for `e_t`**: with a multiplication table of the basis `B` and `0 < t`,
+`esymmCoords tab t zs` has the coordinates of the `t`-th elementary symmetric polynomial of the
+elements with coordinates `zs`. -/
 theorem fieldOfBits_esymmCoords {B : Basis (Fin n) (ZMod 2) F} {tab : List (List (List Bool))}
     (htab : IsMulTable B tab) {t : ℕ} (ht : 0 < t) (zs : List (List Bool)) :
     fieldOfBits B (esymmCoords tab t zs) = (↑(zs.map (fieldOfBits B)) : Multiset F).esymm t := by
@@ -258,6 +263,8 @@ elements. -/
 def traceBit (τ a : List Bool) : Bool :=
   ((List.range τ.length).map fun u => a.getD u false && τ.getD u false).foldl xor false
 
+/-- **The trace as a bit**: with a multiplication table of the basis `B`,
+`traceBit (traceVector tab) a` is the trace over `ZMod 2` of the element with coordinates `a`. -/
 theorem traceBit_traceVector {B : Basis (Fin n) (ZMod 2) F} {tab : List (List (List Bool))}
     (htab : IsMulTable B tab) (a : List Bool) :
     traceBit (traceVector tab) a = bitEquiv (Algebra.trace (ZMod 2) F (fieldOfBits B a)) := by
diff --git a/Complexity/Computability/Complexity/Classes/AWPP.lean b/Complexity/Computability/Complexity/Classes/AWPP.lean
index fd8e84922..72968a7b8 100644
--- a/Complexity/Computability/Complexity/Classes/AWPP.lean
+++ b/Complexity/Computability/Complexity/Classes/AWPP.lean
@@ -48,7 +48,8 @@ open Turing.MultiTapeTM
 
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
-/-- A GapP ratio in `[0, 1]`, at least `2/3` on members and at most `1/3` otherwise. -/
+/-- A GapP ratio in `[0, 1]`, at least `2/3` on members and at most `1/3` otherwise, Fenner's
+characterization of AWPP [Fenner][Fenner2003]. -/
 def AWPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ g ∈ GapP enc, ∃ p : Polynomial ℕ, ∀ a,
     (0 ≤ g a ∧ g a ≤ (2 : ℤ) ^ p.eval (enc a).length) ∧
diff --git a/Complexity/Computability/Complexity/Classes/BPP.lean b/Complexity/Computability/Complexity/Classes/BPP.lean
index 2a0667136..91b3c38e9 100644
--- a/Complexity/Computability/Complexity/Classes/BPP.lean
+++ b/Complexity/Computability/Complexity/Classes/BPP.lean
@@ -47,6 +47,7 @@ The probability is written as a count over the random strings, which are functio
 
 ## References
 
+* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
 -/
 
@@ -72,7 +73,8 @@ def DecidesWithBoundedError (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : 
         V (a, List.ofFn r) = false).card)
 
 /-- The problems decided with bounded error by polynomial-time machines reading polynomially long
-random strings, with respect to the encoding `enc` of instances. -/
+random strings, with respect to the encoding `enc` of instances [Gill][Gill1977],
+[Arora and Barak, Section 7.1][AroraBarak09]. -/
 def BPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTime V (encPair enc encBits) encBool ∧ DecidesWithBoundedError enc p V A}
diff --git a/Complexity/Computability/Complexity/Classes/BooleanHierarchy.lean b/Complexity/Computability/Complexity/Classes/BooleanHierarchy.lean
index 2d4aea1b6..d2625e8c1 100644
--- a/Complexity/Computability/Complexity/Classes/BooleanHierarchy.lean
+++ b/Complexity/Computability/Complexity/Classes/BooleanHierarchy.lean
@@ -198,13 +198,14 @@ private theorem empty_mem_NP : (∅ : Set α) ∈ NP enc :=
 private theorem univ_mem_NP : (Set.univ : Set α) ∈ NP enc :=
   ⟨0, fun _ => true, .const _, by simp [IsVerifier]⟩
 
-/-- The `n`th level of the Boolean hierarchy over NP, with level zero containing only `∅`. -/
+/-- The `n`th level of the Boolean hierarchy over NP, with level zero containing only `∅`
+[Cai et al.][CaiEtAl1988]. -/
 def BH (enc : α ↪ List Bool) (n : ℕ) : Set (Set α) := differenceHierarchy (NP enc) n
 
 /-- The complement of the `n`th level of the Boolean hierarchy over NP. -/
 def coBH (enc : α ↪ List Bool) (n : ℕ) : Set (Set α) := {A | Aᶜ ∈ BH enc n}
 
-/-- The union of all finite levels of the Boolean hierarchy over NP. -/
+/-- The union of all finite levels of the Boolean hierarchy over NP [Cai et al.][CaiEtAl1988]. -/
 def BooleanHierarchy (enc : α ↪ List Bool) : Set (Set α) := ⋃ n, BH enc n
 
 /-- Every finite level belongs to the full Boolean hierarchy. -/
@@ -243,9 +244,11 @@ theorem coBH_zero : coBH enc 0 = {Set.univ} := by
   ext A
   simp [coBH, BH_zero, Set.compl_empty_iff]
 
+/-- The first level is precisely NP. -/
 @[simp]
 theorem BH_one : BH enc 1 = NP enc := differenceHierarchy_one _
 
+/-- The first dual level is precisely coNP. -/
 @[simp]
 theorem coBH_one : coBH enc 1 = coNP enc := by
   ext A
diff --git a/Complexity/Computability/Complexity/Classes/CeqP.lean b/Complexity/Computability/Complexity/Classes/CeqP.lean
index 4743c4fa6..d6a11a3f5 100644
--- a/Complexity/Computability/Complexity/Classes/CeqP.lean
+++ b/Complexity/Computability/Complexity/Classes/CeqP.lean
@@ -43,7 +43,9 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- `C=P`, the zero sets of integer-valued `GapP` functions. -/
+/-- `C=P`, the zero sets of integer-valued `GapP` functions
+[Fenner, Fortnow and Kurtz][FennerFortnowKurtz1994],
+[Fortnow, Classification 4.5][Fortnow1997]. -/
 def CeqP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ g ∈ GapP enc, ∀ a, a ∈ A ↔ g a = 0}
 
diff --git a/Complexity/Computability/Complexity/Classes/DP.lean b/Complexity/Computability/Complexity/Classes/DP.lean
index fe76a7f7d..996009b75 100644
--- a/Complexity/Computability/Complexity/Classes/DP.lean
+++ b/Complexity/Computability/Complexity/Classes/DP.lean
@@ -50,7 +50,8 @@ open Turing.MultiTapeTM
 
 variable {α β γ : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- The class of languages expressible as the intersection of an NP and a coNP language. -/
+/-- The class of languages expressible as the intersection of an NP and a coNP language
+[Papadimitriou][Papadimitriou94]. -/
 def DP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ B ∈ NP enc, ∃ C ∈ coNP enc, A = B ∩ C}
 
diff --git a/Complexity/Computability/Complexity/Classes/EXP.lean b/Complexity/Computability/Complexity/Classes/EXP.lean
index 12c1f6d11..341523fa7 100644
--- a/Complexity/Computability/Complexity/Classes/EXP.lean
+++ b/Complexity/Computability/Complexity/Classes/EXP.lean
@@ -69,7 +69,7 @@ open Turing Turing.MultiTapeTM Filter
 variable {α : Type*} {enc : α ↪ List Bool} {A : Set α}
 
 /-- The problems decidable within time `O(2 ^ n ^ k)` for some `k`, on instances whose encoding
-under `enc` has length `n`. -/
+under `enc` has length `n` [Arora and Barak, Section 2.6][AroraBarak09]. -/
 def EXP (enc : α ↪ List Bool) : Set (Set α) := ⋃ k, DTIME enc fun n => 2 ^ n ^ k
 
 theorem mem_EXP_iff : A ∈ EXP enc ↔ ∃ k, A ∈ DTIME enc fun n => 2 ^ n ^ k :=
@@ -83,7 +83,8 @@ theorem mem_E_iff : A ∈ E enc ↔ ∃ k, A ∈ DTIME enc fun n => 2 ^ (k * n)
   Set.mem_iUnion
 
 /-- The problems decidable by a nondeterministic machine within time `O(2 ^ n ^ k)` for some `k`,
-on instances whose encoding under `enc` has length `n`. -/
+on instances whose encoding under `enc` has length `n`
+[Arora and Barak, Section 2.6][AroraBarak09]. -/
 def NEXP (enc : α ↪ List Bool) : Set (Set α) := ⋃ k, NTIME enc fun n => 2 ^ n ^ k
 
 theorem mem_NEXP_iff : A ∈ NEXP enc ↔ ∃ k, A ∈ NTIME enc fun n => 2 ^ n ^ k :=
@@ -131,10 +132,12 @@ theorem NE_subset_NEXP : NE enc ⊆ NEXP enc := fun _ hA =>
 theorem NP_subset_NEXP {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ NEXP enc :=
   NP_subset_NE.trans NE_subset_NEXP
 
+/-- **Linear exponential time is within nondeterministic linear exponential time.** -/
 theorem E_subset_NE : E enc ⊆ NE enc := fun _ hA =>
   let ⟨k, hk⟩ := mem_E_iff.mp hA
   mem_NE_iff.mpr ⟨k, DTIME_subset_NTIME hk⟩
 
+/-- **Exponential time is within nondeterministic exponential time.** -/
 theorem EXP_subset_NEXP : EXP enc ⊆ NEXP enc := fun _ hA =>
   let ⟨k, hk⟩ := mem_EXP_iff.mp hA
   mem_NEXP_iff.mpr ⟨k, DTIME_subset_NTIME hk⟩
diff --git a/Complexity/Computability/Complexity/Classes/FewP.lean b/Complexity/Computability/Complexity/Classes/FewP.lean
index 450b70e55..8e83bc368 100644
--- a/Complexity/Computability/Complexity/Classes/FewP.lean
+++ b/Complexity/Computability/Complexity/Classes/FewP.lean
@@ -51,7 +51,8 @@ open Turing.MultiTapeTM
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α}
 
 /-- A language in NP with a polynomial bound on the number of accepting certificates on every
-input. The bound is in the encoded input length, not in the certificate length. -/
+input [Allender and Rubinstein][AllenderRubinstein1988]. The bound is in the encoded input length,
+not in the certificate length. -/
 def FewP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, ∃ p : Polynomial ℕ,
     (∀ a, f a ≤ p.eval (enc a).length) ∧ ∀ a, a ∈ A ↔ 0 < f a}
diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean
index 06b4632a7..06fcee565 100644
--- a/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean
+++ b/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean
@@ -29,6 +29,11 @@ which is `O(|x|)`. Padded descriptions are short.
   description with the number of binary digits of the length of the word.
 * `Cslib.Complexity.Diagonal.computableTidilyInO_shortDesc`: shortness is decided within quadratic
   time and linear space.
+
+## References
+
+* [M. Sipser, *Introduction to the Theory of Computation*, Theorems 9.3 and 9.10][Sipser2013]:
+  the padded descriptions in the proofs of the hierarchy theorems.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean b/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean
index b9bcfdbfd..a8cfe7659 100644
--- a/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean
+++ b/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean
@@ -520,6 +520,8 @@ theorem acceptProb_round_prover {x : Graph × Graph} (hx : x ∈ GraphNonIsomorp
   obtain ⟨σ, hσ⟩ := exists_equiv_of_mem_support_relabelDist hm hm'
   exact mem_GraphIsomorphism_iff.2 ⟨σ, hσ⟩
 
+/-- One round is an interactive proof for `GraphNonIsomorphism` with completeness `1` and
+soundness error `17 / 32`. -/
 theorem isInteractiveProof_round :
     IsInteractiveProof round GraphNonIsomorphism 1 (17 / 32) where
   complete x hx := ⟨prover x, (acceptProb_round_prover hx).ge⟩
@@ -537,6 +539,8 @@ theorem acceptProb_verifier_le {x : Graph × Graph} (hx : x ∈ GraphIsomorphism
     acceptProb (verifier x) P ≤ (17 / 32) ^ 2 :=
   acceptProb_sequentialRepeat_le (acceptProb_round_le hx) 2 P
 
+/-- The verifier, two sequential rounds, is an interactive proof for `GraphNonIsomorphism` with
+completeness `1` and soundness error `(17 / 32) ^ 2`. -/
 theorem isInteractiveProof_verifier :
     IsInteractiveProof verifier GraphNonIsomorphism 1 ((17 / 32) ^ 2) where
   complete x hx := ⟨prover x, (acceptProb_verifier_prover hx).ge⟩
diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean
index 2f64cb268..7244bf49b 100644
--- a/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean
+++ b/Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean
@@ -61,6 +61,12 @@ All are polynomial-time in their unary or binary inputs.
 * `Cslib.Complexity.QBFProtocol.updatePt_canonPt`: updating a point.
 * `Cslib.Complexity.QBFProtocol.decodeReply_encodeReply`: decoding inverts the honest encoding.
 * `Cslib.Complexity.QBFProtocol.eval_sampleMod_le`: the samples are nearly uniform.
+
+## References
+
+* [A. Shamir, *IP = PSPACE*][Shamir1992]
+* [A. Shen, *IP = SPACE: simplified proof*][Shen1992]
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 8.3][AroraBarak09]
 -/
 
 @[expose] public section
@@ -106,6 +112,7 @@ theorem natCast_connectiveMod [NeZero p] (o : ArithQBF.Connective) (a b : ℕ) :
   · rw [connectiveMod, natCast_subMod, Nat.cast_mul, natCast_subMod, natCast_subMod,
       ArithQBF.Connective.apply, Nat.cast_one]
 
+/-- For `p ≠ 0`, `operatorMod` computes the operators of the arithmetization in `ZMod p`. -/
 theorem natCast_operatorMod [NeZero p] (o : ArithQBF.Operator) (t a b : ℕ) :
     ((operatorMod p o t a b : ℕ) : ZMod p) = o.apply (t : ZMod p) a b := by
   cases o
@@ -115,6 +122,8 @@ theorem natCast_operatorMod [NeZero p] (o : ArithQBF.Operator) (t a b : ℕ) :
   · rw [operatorMod, ZMod.natCast_mod, Nat.cast_add, Nat.cast_mul, Nat.cast_mul, natCast_subMod,
       ArithQBF.Operator.apply, Nat.cast_one]
 
+/-- For `p ≠ 0`, Horner's rule modulo `p` evaluates the coefficient list `l` at `z` in
+`ZMod p`. -/
 theorem natCast_hornerMod [NeZero p] (z : ℕ) (l : List ℕ) :
     ((hornerMod p z l : ℕ) : ZMod p) = evalCoeffList (z : ZMod p) (l.map Nat.cast) := by
   rw [hornerMod, List.foldl_reverse, Nat.sub_add_cancel NeZero.one_le]
@@ -188,6 +197,8 @@ theorem normPt_canonPt [NeZero p] (xs : List ℕ) (r : ℕ → ZMod p) :
   refine List.map_congr_left fun x hx => ?_
   rw [lookupPt_canonPt r hx, Nat.mod_eq_of_lt (ZMod.val_lt _)]
 
+/-- For `p ≠ 0`, setting the variable `v` to `z` in the point `r` on the variables of `xs` gives
+the point `Function.update r v z` on the same variables. -/
 theorem updatePt_canonPt [NeZero p] (xs : List ℕ) (r : ℕ → ZMod p) (v z : ℕ) :
     updatePt p xs (canonPt xs r) v z = canonPt xs (Function.update r v (z : ZMod p)) := by
   unfold updatePt canonPt
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace.lean b/Complexity/Computability/Complexity/Classes/LogSpace.lean
index 870431c80..f58397bf5 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace.lean
+++ b/Complexity/Computability/Complexity/Classes/LogSpace.lean
@@ -107,7 +107,8 @@ variable {α β γ : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {e
   {A : Set α} {B : Set β} {C : Set γ}
 
 /-- The problems decided in logarithmic space with respect to the encoding `enc`: a Boolean
-function deciding membership is computable in logarithmic space. -/
+function deciding membership is computable in logarithmic space
+[Sipser, Section 8.4][Sipser2013]. -/
 def L (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f : α → Bool, ComputableInLogSpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true}
 
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean
index 344a1f164..736386338 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean
@@ -46,7 +46,8 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
-/-- The problems whose complements belong to native nondeterministic logarithmic space. -/
+/-- The problems whose complements belong to native nondeterministic logarithmic space
+[Sipser, Section 8.6][Sipser2013]. -/
 def coNL (enc : α ↪ List Bool) : Set (Set α) := {A | Aᶜ ∈ NL enc}
 
 /-- A problem belongs to `coNL` exactly when its complement belongs to `NL`. -/
diff --git a/Complexity/Computability/Complexity/Classes/ModP.lean b/Complexity/Computability/Complexity/Classes/ModP.lean
index 98bb25115..9c8392e7b 100644
--- a/Complexity/Computability/Complexity/Classes/ModP.lean
+++ b/Complexity/Computability/Complexity/Classes/ModP.lean
@@ -53,8 +53,8 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α} {k : ℕ}
 
-/-- For a fixed modulus `k`, languages recognized by a nonzero residue of a `#P` count. The
-standard modular counting classes use `k ≥ 2`. -/
+/-- For a fixed modulus `k`, languages recognized by a nonzero residue of a `#P` count
+[Fortnow, Classification 4.7][Fortnow1997]. The standard modular counting classes use `k ≥ 2`. -/
 def ModP (k : ℕ) (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, ∀ a, a ∈ A ↔ f a % k ≠ 0}
 
diff --git a/Complexity/Computability/Complexity/Classes/NP.lean b/Complexity/Computability/Complexity/Classes/NP.lean
index 5acb10fdb..cb2d0d768 100644
--- a/Complexity/Computability/Complexity/Classes/NP.lean
+++ b/Complexity/Computability/Complexity/Classes/NP.lean
@@ -78,7 +78,7 @@ def IsVerifier (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Boo
   ∀ a, a ∈ A ↔ ∃ w : List Bool, w.length = p.eval (enc a).length ∧ V (a, w) = true
 
 /-- The problems with polynomial-time verifiers and polynomially long certificates, with respect to
-the encoding `enc` of instances. -/
+the encoding `enc` of instances [Arora and Barak, Definition 2.1][AroraBarak09]. -/
 def NP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsVerifier enc p V A}
@@ -136,7 +136,7 @@ theorem IsVerifier.guard {c : α → Bool} (h : IsVerifier enc p V A) :
 
 end Padding
 
-/-- The problems whose complements are in `NP`. -/
+/-- The problems whose complements are in `NP` [Arora and Barak, Section 2.6][AroraBarak09]. -/
 def coNP (enc : α ↪ List Bool) : Set (Set α) := {A | Aᶜ ∈ NP enc}
 
 theorem mem_coNP {enc : α ↪ List Bool} {A : Set α} : A ∈ coNP enc ↔ Aᶜ ∈ NP enc := Iff.rfl
diff --git a/Complexity/Computability/Complexity/Classes/Operators.lean b/Complexity/Computability/Complexity/Classes/Operators.lean
index 91254f68f..898fde6cb 100644
--- a/Complexity/Computability/Complexity/Classes/Operators.lean
+++ b/Complexity/Computability/Complexity/Classes/Operators.lean
@@ -63,7 +63,8 @@ variable {α : Type}
 open Classical in
 /-- **The parity operator `⊕·C`**: the problems `L` such that, for some `L' ∈ C` and polynomial
 `p`, `a ∈ L` exactly when an odd number of the strings `w` of length `p (enc a).length` have
-`(a, w) ∈ L'`. The problems of `C` are about pairs of an instance and a string. -/
+`(a, w) ∈ L'`. The problems of `C` are about pairs of an instance and a string
+[Toda][Toda1991]. -/
 def ParityOp (enc : α ↪ List Bool) (C : Set (Set (α × List Bool))) : Set (Set α) :=
   {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C,
     ∀ a, a ∈ L ↔ Odd (acceptCount (fun x => decide (x ∈ L')) a (p.eval (enc a).length))}
@@ -73,7 +74,7 @@ open Classical in
 polynomial `p`, membership in `L'` decides `L` with bounded error using random strings of length
 `p (enc a).length`: for every instance `a`, at least two thirds of the random strings `r` have
 `(a, r) ∈ L'` exactly when `a ∈ L`. The problems of `C` are about pairs of an instance and a
-string. -/
+string [Schöning][Schoening1989], [Toda][Toda1991]. -/
 def BPOp (enc : α ↪ List Bool) (C : Set (Set (α × List Bool))) : Set (Set α) :=
   {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, DecidesWithBoundedError enc p (fun x => decide (x ∈ L')) L}
 
diff --git a/Complexity/Computability/Complexity/Classes/Oracle.lean b/Complexity/Computability/Complexity/Classes/Oracle.lean
index b7d8e1d97..de1670a99 100644
--- a/Complexity/Computability/Complexity/Classes/Oracle.lean
+++ b/Complexity/Computability/Complexity/Classes/Oracle.lean
@@ -164,7 +164,7 @@ theorem interpret_languageOracle_congr {A B : Set (List Bool)} (program : WordQu
 /-- `f` is computable in polynomial time relative to the oracle language `A`: a deterministic
 word-query program computes `f` against `A`, and one finite machine under one polynomial clock
 realizes the program against every stateful oracle, charging request construction and reply
-access. -/
+access. This is the oracle Turing machine of [Arora and Barak, Section 3.4][AroraBarak09]. -/
 @[fun_prop]
 def ComputableInPolyTimeWithOracle (A : Set (List Bool)) (f : α → β) (input : α ↪ List Bool)
     (output : β ↪ List Bool) : Prop :=
@@ -182,7 +182,8 @@ theorem _root_.Turing.MultiTapeTM.ComputableTidilyInPolyTime.computableInPolyTim
   ⟨fun a => pure (f a), h.isOraclePPTOn, fun _ => rfl⟩
 
 /-- The problems decidable in polynomial time relative to the oracle language `A`, with respect to
-the encoding `enc` of instances: `Cslib.Complexity.P` with an oracle. -/
+the encoding `enc` of instances: `Cslib.Complexity.P` with an oracle
+[Arora and Barak, Section 3.4][AroraBarak09]. -/
 def PWithOracle (A : Set (List Bool)) (enc : α ↪ List Bool) : Set (Set α) :=
   {L | ∃ f : α → Bool, ComputableInPolyTimeWithOracle A f enc encBool ∧ ∀ a, a ∈ L ↔ f a = true}
 
@@ -192,7 +193,8 @@ theorem mem_PWithOracle {A : Set (List Bool)} {enc : α ↪ List Bool} {L : Set
   Iff.rfl
 
 /-- The problems with verifiers computable in polynomial time relative to the oracle language `A`
-and polynomially long certificates: `Cslib.Complexity.NP` with an oracle. -/
+and polynomially long certificates: `Cslib.Complexity.NP` with an oracle
+[Arora and Barak, Section 3.4][AroraBarak09]. -/
 def NPWithOracle (A : Set (List Bool)) (enc : α ↪ List Bool) : Set (Set α) :=
   {L | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTimeWithOracle A V (encPair enc encBits) encBool ∧ IsVerifier enc p V L}
diff --git a/Complexity/Computability/Complexity/Classes/Oracle/Counting.lean b/Complexity/Computability/Complexity/Classes/Oracle/Counting.lean
index 4251fd0ee..28f4f7891 100644
--- a/Complexity/Computability/Complexity/Classes/Oracle/Counting.lean
+++ b/Complexity/Computability/Complexity/Classes/Oracle/Counting.lean
@@ -83,10 +83,10 @@ theorem answersBits_bitGraph (encβ : β ↪ List Bool) (f : β → ℕ) :
   (encPair encβ encNat).injective.mem_set_image
 
 open Classical in
-/-- **`P^#P`**: the problems `L` such that, for some type `β` with encoding `encβ` and some
-`f ∈ SharpP encβ`, one deterministic oracle program, strict oracle PPT on the encoding `enc` of
-instances, decides `L` against every oracle language answering the bits of `f`. Answers on
-words that are not codes are arbitrary. -/
+/-- **`P^#P`** [Arora and Barak, Chapter 17][AroraBarak09]: the problems `L` such that, for some
+type `β` with encoding `encβ` and some `f ∈ SharpP encβ`, one deterministic oracle program, strict
+oracle PPT on the encoding `enc` of instances, decides `L` against every oracle language answering
+the bits of `f`. Answers on words that are not codes are arbitrary. -/
 def PWithSharpPOracle (enc : α ↪ List Bool) : Set (Set α) :=
   {L | ∃ (β : Type) (encβ : β ↪ List Bool) (f : β → ℕ), f ∈ SharpP encβ ∧
     ∃ program : α → WordQueryComp Unit Bool,
diff --git a/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean b/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean
index efbbb4af3..2ab32b1bc 100644
--- a/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean
+++ b/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean
@@ -202,6 +202,7 @@ def tokensDecoder : Decoder (encList encToken) := .list (.pair kindDecoder .nat)
 /-- Whether a token list is the token list of a formula. -/
 def wellFormed (ts : List (QBF.Kind × ℕ)) : Bool := decide (ts.foldl wfStep (true, 1) = (true, 0))
 
+/-- `wellFormed ts` holds exactly when `ts` is the token list of a formula. -/
 theorem wellFormed_iff (ts : List (QBF.Kind × ℕ)) :
     wellFormed ts = true ↔ ∃ φ : QBF ℕ, φ.tokens = ts := by
   rw [wellFormed, decide_eq_true_iff, foldl_wfStep_eq_iff]
@@ -261,6 +262,7 @@ to the word. -/
 def isCode (w : List Bool) : Bool :=
   wellFormed (tokensDecoder.decode w) && decide (encList encToken (tokensDecoder.decode w) = w)
 
+/-- A word passes `isCode` exactly when it encodes a formula. -/
 theorem isCode_iff (w : List Bool) : isCode w = true ↔ ∃ φ, encQBF φ = w := by
   unfold isCode
   rw [Bool.and_eq_true, wellFormed_iff, decide_eq_true_iff]
@@ -271,6 +273,7 @@ theorem isCode_iff (w : List Bool) : isCode w = true ↔ ∃ φ, encQBF φ = w :
     rw [encQBF_apply, tokensDecoder.decode_enc]
     exact ⟨⟨φ, rfl⟩, rfl⟩
 
+/-- Whether a word encodes a formula is decidable in polynomial time. -/
 theorem isCode_pt : ComputableTidilyInPolyTime isCode encBits encBool := by
   obtain ⟨d, e, hD⟩ := tokensDecoder.computable
   have hD := hD.computableTidilyInPolyTime
@@ -294,6 +297,7 @@ theorem encQBF_decodeQBF (w : List Bool) :
   · exact absurd ((isCode_iff w).mp h₃) h₁
   · rfl
 
+/-- `decodeQBF` is polynomial-time. -/
 theorem decodeQBF_pt : ComputableTidilyInPolyTime decodeQBF encBits encQBF :=
   (ComputableTidilyInPolyTime.ite' isCode_pt ComputableTidilyInPolyTime.id'
     (ComputableTidilyInPolyTime.const (encQBF .bot))).of_enc_eq fun w => encQBF_decodeQBF w
diff --git a/Complexity/Computability/Complexity/Classes/P.lean b/Complexity/Computability/Complexity/Classes/P.lean
index eed0fcb22..8d171a1b4 100644
--- a/Complexity/Computability/Complexity/Classes/P.lean
+++ b/Complexity/Computability/Complexity/Classes/P.lean
@@ -65,7 +65,8 @@ open Turing.MultiTapeTM
 variable {α : Type*}
 
 /-- The problems decidable in polynomial time with respect to the encoding `enc`: `A ∈ P enc`
-when a Boolean function deciding membership in `A` is computable in polynomial time. -/
+when a Boolean function deciding membership in `A` is computable in polynomial time
+[Arora and Barak, Definition 1.13][AroraBarak09]. -/
 def P (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f : α → Bool, ComputableInPolyTime f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true}
 
diff --git a/Complexity/Computability/Complexity/Classes/PCP.lean b/Complexity/Computability/Complexity/Classes/PCP.lean
index 100b6d396..66e869517 100644
--- a/Complexity/Computability/Complexity/Classes/PCP.lean
+++ b/Complexity/Computability/Complexity/Classes/PCP.lean
@@ -114,7 +114,8 @@ def IsPCPVerifier (enc : α ↪ List Bool) (r q : ℕ → ℕ) (V : PCPVerifier
 
 /-- The class `PCP(r, q)` with respect to the encoding `enc` of instances: the problems with a
 polynomial-time verifier using `O(r n)` random bits and `O(q n)` queries on instances whose
-encoding has length `n`. -/
+encoding has length `n` [Arora and Safra][AroraSafra1998],
+[Arora and Barak, Chapter 11][AroraBarak09]. -/
 def PCP (r q : ℕ → ℕ) (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (V : PCPVerifier α) (c d : ℕ), V.PolyTime enc ∧
     IsPCPVerifier enc (fun n => c * r n) (fun n => d * q n) V A}
diff --git a/Complexity/Computability/Complexity/Classes/PH.lean b/Complexity/Computability/Complexity/Classes/PH.lean
index f30d551a3..d51ac907d 100644
--- a/Complexity/Computability/Complexity/Classes/PH.lean
+++ b/Complexity/Computability/Complexity/Classes/PH.lean
@@ -18,7 +18,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Ba
 
 The levels `Σₖ` and `Πₖ` of the polynomial hierarchy are defined like `NP`
 (`Cslib.Complexity.NP`), through polynomial-time verifiers, now with `k` alternating quantifiers
-over certificates [Arora and Barak, Definition 5.4][AroraBarak09], [Wrathall][Wrathall1976]:
+over certificates [Arora and Barak, Definition 5.3][AroraBarak09], [Wrathall][Wrathall1976]:
 `A ∈ SigmaP k enc` when there are polynomials `p₁, …, pₖ` and a function
 `V : α × List Bool → Bool`, computable in polynomial time on inputs
 `encPair enc encBits (a, w) = frame (enc a) ++ w`, such that
@@ -190,7 +190,8 @@ theorem isAlternatingVerifier_true_singleton {p : Polynomial ℕ} :
 
 /-- The level `Σₖ` of the polynomial hierarchy, with respect to the encoding `enc` of instances:
 the problems verified in polynomial time through `k` alternating blocks of polynomially long
-certificates, the first existential. -/
+certificates, the first existential [Arora and Barak, Definition 5.3][AroraBarak09],
+[Wrathall][Wrathall1976]. -/
 def SigmaP (k : ℕ) (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool), ps.length = k ∧
     ComputableInPolyTime V (encPair enc encBits) encBool ∧
@@ -198,13 +199,15 @@ def SigmaP (k : ℕ) (enc : α ↪ List Bool) : Set (Set α) :=
 
 /-- The level `Πₖ` of the polynomial hierarchy, with respect to the encoding `enc` of instances:
 the problems verified in polynomial time through `k` alternating blocks of polynomially long
-certificates, the first universal. -/
+certificates, the first universal [Arora and Barak, Definition 5.3][AroraBarak09],
+[Wrathall][Wrathall1976]. -/
 def PiP (k : ℕ) (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (ps : List (Polynomial ℕ)) (V : α × List Bool → Bool), ps.length = k ∧
     ComputableInPolyTime V (encPair enc encBits) encBool ∧
       IsAlternatingVerifier enc false ps V A}
 
-/-- The polynomial hierarchy: the union of the levels `Σₖ`. -/
+/-- The polynomial hierarchy: the union of the levels `Σₖ` [Stockmeyer][Stockmeyer1976],
+[Arora and Barak, Definition 5.3][AroraBarak09]. -/
 def PH (enc : α ↪ List Bool) : Set (Set α) := ⋃ k, SigmaP k enc
 
 variable {k : ℕ}
@@ -235,6 +238,7 @@ theorem mem_PiP_iff_tidy : A ∈ PiP k enc ↔
         IsAlternatingVerifier enc false ps V A := by
   simp only [mem_PiP, computableInPolyTime_iff_computableTidilyInPolyTime]
 
+/-- A problem is in the polynomial hierarchy exactly when it is in some level `Σₖ`. -/
 theorem mem_PH : A ∈ PH enc ↔ ∃ k, A ∈ SigmaP k enc := Set.mem_iUnion
 
 /-! ### The first levels -/
@@ -277,15 +281,19 @@ theorem PiP_zero : PiP 0 enc = P enc :=
 
 /-! ### Inclusions between levels -/
 
+/-- `Σₖ ⊆ Σₖ₊₁`: a block of certificates of length `0` is added at the end. -/
 theorem SigmaP_subset_SigmaP_succ (k : ℕ) : SigmaP k enc ⊆ SigmaP (k + 1) enc :=
   fun _ ⟨ps, V, hk, hV, h⟩ => ⟨ps ++ [0], V, by simp [hk], hV, h.append_zero⟩
 
+/-- `Πₖ ⊆ Πₖ₊₁`: a block of certificates of length `0` is added at the end. -/
 theorem PiP_subset_PiP_succ (k : ℕ) : PiP k enc ⊆ PiP (k + 1) enc :=
   fun _ ⟨ps, V, hk, hV, h⟩ => ⟨ps ++ [0], V, by simp [hk], hV, h.append_zero⟩
 
+/-- `Σₖ ⊆ Πₖ₊₁`: a universal block of certificates of length `0` is added at the start. -/
 theorem SigmaP_subset_PiP_succ (k : ℕ) : SigmaP k enc ⊆ PiP (k + 1) enc :=
   fun _ ⟨ps, V, hk, hV, h⟩ => ⟨0 :: ps, V, by simp [hk], hV, h.zero_cons⟩
 
+/-- `Πₖ ⊆ Σₖ₊₁`: an existential block of certificates of length `0` is added at the start. -/
 theorem PiP_subset_SigmaP_succ (k : ℕ) : PiP k enc ⊆ SigmaP (k + 1) enc :=
   fun _ ⟨ps, V, hk, hV, h⟩ => ⟨0 :: ps, V, by simp [hk], hV, h.zero_cons⟩
 
@@ -307,8 +315,10 @@ theorem PH_eq_iUnion_PiP : PH enc = ⋃ k, PiP k enc :=
     (SigmaP_subset_PiP_succ k).trans (Set.subset_iUnion (fun k => PiP k enc) (k + 1))).antisymm
     (Set.iUnion_subset PiP_subset_PH)
 
+/-- `NP ⊆ PH`, since `NP = Σ₁`. -/
 theorem NP_subset_PH : NP enc ⊆ PH enc := SigmaP_one (enc := enc) ▸ SigmaP_subset_PH 1
 
+/-- `P ⊆ PH`, since `P ⊆ Σ₀`. -/
 theorem P_subset_PH : P enc ⊆ PH enc :=
   P_subset_SigmaP_zero.trans (SigmaP_subset_PH 0)
 
@@ -338,6 +348,7 @@ theorem SigmaP_eq_preimage_compl_PiP : SigmaP k enc = compl ⁻¹' PiP k enc :=
 theorem PiP_one_eq_coNP : PiP 1 enc = coNP enc := by
   rw [PiP_eq_preimage_compl_SigmaP, SigmaP_one, coNP_eq_preimage_compl_NP]
 
+/-- `coNP ⊆ PH`, since `coNP = Π₁`. -/
 theorem coNP_subset_PH : coNP enc ⊆ PH enc :=
   PiP_one_eq_coNP ▸ PiP_subset_PH 1
 
diff --git a/Complexity/Computability/Complexity/Classes/PP.lean b/Complexity/Computability/Complexity/Classes/PP.lean
index 1b755b732..a958210cc 100644
--- a/Complexity/Computability/Complexity/Classes/PP.lean
+++ b/Complexity/Computability/Complexity/Classes/PP.lean
@@ -62,7 +62,7 @@ def DecidesByMajority (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × L
   ∀ a, a ∈ A ↔ 2 ^ p.eval (enc a).length < 2 * acceptCount V a (p.eval (enc a).length)
 
 /-- The problems decided by majority by polynomial-time machines reading polynomially long random
-strings, with respect to the encoding `enc` of instances. -/
+strings, with respect to the encoding `enc` of instances [Gill][Gill1977]. -/
 def PP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTime V (encPair enc encBits) encBool ∧ DecidesByMajority enc p V A}
diff --git a/Complexity/Computability/Complexity/Classes/ParityP.lean b/Complexity/Computability/Complexity/Classes/ParityP.lean
index 2a5d91a8d..6d5650ee2 100644
--- a/Complexity/Computability/Complexity/Classes/ParityP.lean
+++ b/Complexity/Computability/Complexity/Classes/ParityP.lean
@@ -122,7 +122,9 @@ theorem computableTidilyInPolyTime_succVerifier {enc : α ↪ List Bool}
 
 /-- **The class `⊕P`**: the parity operator applied to `P`. A problem `L` is in `⊕P` when, for a
 polynomial `p` and a polynomial-time `V`, `a ∈ L` exactly when an odd number of the strings `w` of
-length `p (enc a).length` have `V (a, w) = true` (`mem_ParityP`). -/
+length `p (enc a).length` have `V (a, w) = true` (`mem_ParityP`)
+[Papadimitriou and Zachos][PapadimitriouZachos1983],
+[Arora and Barak, Section 17.4][AroraBarak09]. -/
 def ParityP (enc : α ↪ List Bool) : Set (Set α) := ParityOp enc (P (encPair enc encBits))
 
 variable {enc : α ↪ List Bool} {L : Set α}
diff --git a/Complexity/Computability/Complexity/Classes/Promise/Basic.lean b/Complexity/Computability/Complexity/Classes/Promise/Basic.lean
index 0a6dde77a..fb66a6c13 100644
--- a/Complexity/Computability/Complexity/Classes/Promise/Basic.lean
+++ b/Complexity/Computability/Complexity/Classes/Promise/Basic.lean
@@ -149,6 +149,8 @@ theorem promiseClass_injective : Function.Injective (promiseClass (α := α)) :=
   (promiseClass_subset_promiseClass_iff.1 h.le).antisymm
     (promiseClass_subset_promiseClass_iff.1 h.ge)
 
+/-- Two classes of decision problems have the same lift to promise problems exactly when they are
+equal. -/
 theorem promiseClass_inj : promiseClass C = promiseClass D ↔ C = D :=
   promiseClass_injective.eq_iff
 
@@ -183,7 +185,7 @@ section PromiseP
 variable {α : Type*} {enc : α ↪ List Bool} {Q : PromiseProblem α}
 
 /-- The promise problems solved by polynomial-time algorithms, with respect to the encoding `enc`
-of instances: the lift of `P enc`. -/
+of instances: the lift of `P enc` [Goldreich][Goldreich2006]. -/
 def PromiseP (enc : α ↪ List Bool) : Set (PromiseProblem α) := promiseClass (P enc)
 
 /-- **Goldreich's definition of promise-P**: a promise problem is in `PromiseP` when a
@@ -202,7 +204,7 @@ section PromiseNP
 variable {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α}
 
 /-- The promise problems with polynomial-time verifiers, with respect to the encoding `enc` of
-instances: the lift of `NP enc`. -/
+instances: the lift of `NP enc` [Goldreich][Goldreich2006]. -/
 def PromiseNP (enc : α ↪ List Bool) : Set (PromiseProblem α) := promiseClass (NP enc)
 
 /-- **Goldreich's definition of promise-NP**: a promise problem is in `PromiseNP` when a
diff --git a/Complexity/Computability/Complexity/Classes/RP.lean b/Complexity/Computability/Complexity/Classes/RP.lean
index 75499fd0d..10a8a344b 100644
--- a/Complexity/Computability/Complexity/Classes/RP.lean
+++ b/Complexity/Computability/Complexity/Classes/RP.lean
@@ -76,13 +76,14 @@ def DecidesWithOneSidedError (enc : α ↪ List Bool) (p : Polynomial ℕ) (V :
     (a ∉ A → ∀ r : Fin (p.eval (enc a).length) → Bool, V (a, List.ofFn r) = false)
 
 /-- The problems decided with one-sided error by polynomial-time machines reading polynomially
-long random strings, with respect to the encoding `enc` of instances. -/
+long random strings, with respect to the encoding `enc` of instances
+[Arora and Barak, Section 7.3][AroraBarak09]. -/
 def RP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTime V (encPair enc encBits) encBool ∧
       DecidesWithOneSidedError enc p V A}
 
-/-- The problems whose complements are in `RP`. -/
+/-- The problems whose complements are in `RP` [Arora and Barak, Section 7.3][AroraBarak09]. -/
 def coRP (enc : α ↪ List Bool) : Set (Set α) := {A | Aᶜ ∈ RP enc}
 
 variable {enc : α ↪ List Bool}
@@ -122,8 +123,10 @@ theorem DecidesWithOneSidedError.isVerifier {p : Polynomial ℕ} {V : α × List
     rw [hV] at this
     exact Bool.noConfusion this
 
+/-- `RP ⊆ NP`: a random string accepted by a one-sided-error decider is a certificate. -/
 theorem RP_subset_NP : RP enc ⊆ NP enc := fun _ ⟨p, V, hV, h⟩ => ⟨p, V, hV, h.isVerifier⟩
 
+/-- `coRP ⊆ coNP`. -/
 theorem coRP_subset_coNP : coRP enc ⊆ coNP enc := fun _ hA => RP_subset_NP hA
 
 /-! ### Error reduction -/
diff --git a/Complexity/Computability/Complexity/Classes/SBP.lean b/Complexity/Computability/Complexity/Classes/SBP.lean
index cfad7caf5..6e0cc407e 100644
--- a/Complexity/Computability/Complexity/Classes/SBP.lean
+++ b/Complexity/Computability/Complexity/Classes/SBP.lean
@@ -59,7 +59,8 @@ open Turing.MultiTapeTM
 
 variable {α β : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- A #P count at least an FP threshold on members and strictly below half on nonmembers.
+/-- A #P count at least an FP threshold on members and strictly below half on nonmembers
+[Böhler, Glaßer and Meister][BoehlerGlasserMeister2006], [Watson, Definition 2][Watson2012].
 The threshold is encoded in binary and may be exponentially large. -/
 def SBP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, ∃ k : α → ℕ, ComputableInPolyTime k enc encNat ∧
diff --git a/Complexity/Computability/Complexity/Classes/SPP.lean b/Complexity/Computability/Complexity/Classes/SPP.lean
index 3996b01fb..abe078bbf 100644
--- a/Complexity/Computability/Complexity/Classes/SPP.lean
+++ b/Complexity/Computability/Complexity/Classes/SPP.lean
@@ -44,7 +44,8 @@ open scoped symmDiff
 
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- Small-gap polynomial time: a GapP function is one on members and zero on nonmembers. -/
+/-- Small-gap polynomial time: a GapP function is one on members and zero on nonmembers
+[Fenner, Fortnow and Kurtz][FennerFortnowKurtz1994], [Fortnow, Classification 4.4][Fortnow1997]. -/
 def SPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ GapP enc, (∀ a, f a = 0 ∨ f a = 1) ∧ ∀ a, a ∈ A ↔ f a = 1}
 
diff --git a/Complexity/Computability/Complexity/Classes/Space.lean b/Complexity/Computability/Complexity/Classes/Space.lean
index d037b0ee7..44f9038cd 100644
--- a/Complexity/Computability/Complexity/Classes/Space.lean
+++ b/Complexity/Computability/Complexity/Classes/Space.lean
@@ -86,7 +86,7 @@ variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 /-- The problems decided by one deterministic machine within polynomial space, with respect to
 the encoding `enc`: a Boolean function deciding membership is computable (upstream
 `Turing.MultiTapeTM.ComputableInTimeAndSpace`) within some time and within space polynomially
-bounded in the length of the encoded instance. -/
+bounded in the length of the encoded instance [Sipser, Section 8.2][Sipser2013]. -/
 def PSPACE (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f : α → Bool, (∃ t s, PolyBounded (fun a => (enc a).length) s ∧
     ComputableInTimeAndSpace f enc encBool t s) ∧ ∀ a, a ∈ A ↔ f a = true}
@@ -124,7 +124,8 @@ theorem mem_PSPACE_iff_exists_mem_DSPACE {α : Type} {enc : α ↪ List Bool} {A
 /-- The problems decided by one nondeterministic machine within polynomial space, with respect to
 the encoding `enc` (`Turing.MultiTapeNTM.DecidesInSpace`): every computation path on `enc a`
 visits at most `s a` work-tape cells, for a polynomially bounded `s`, every branch halts, and
-`a ∈ A` exactly when some computation path halts with output `[true]`. -/
+`a ∈ A` exactly when some computation path halts with output `[true]`
+[Sipser, Section 8.2][Sipser2013]. -/
 def NPSPACE (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : MultiTapeNTM k Bool State)
     (s : α → ℕ), PolyBounded (fun a => (enc a).length) s ∧ ntm.DecidesInSpace enc A s}
diff --git a/Complexity/Computability/Complexity/Classes/Space/Basic.lean b/Complexity/Computability/Complexity/Classes/Space/Basic.lean
index 5153f04fe..4d0d2b203 100644
--- a/Complexity/Computability/Complexity/Classes/Space/Basic.lean
+++ b/Complexity/Computability/Complexity/Classes/Space/Basic.lean
@@ -49,7 +49,7 @@ variable {α : Type*} {enc : α ↪ List Bool} {A : Set α}
 
 /-- The problems decidable within space `O(s n)`, that is `c₁ * s n + c₂` for constants `c₁` and
 `c₂`, on instances whose encoding under `enc` has length `n`, by a machine with a binary alphabet
-and finitely many states, within some time bound of `n`. -/
+and finitely many states, within some time bound of `n` [Sipser, Definition 8.2][Sipser2013]. -/
 def DSPACE (enc : α ↪ List Bool) (s : ℕ → ℕ) : Set (Set α) :=
   {A | ∃ c₁ c₂ : ℕ, ∃ t : ℕ → ℕ,
     DecidableInTimeAndSpace A enc (fun a => t (enc a).length) fun a => c₁ * s (enc a).length + c₂}
diff --git a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean
index fd0b9aca4..c5cc36a99 100644
--- a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean
+++ b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean
@@ -135,6 +135,10 @@ section Arcs
 
 variable {xs : List ℕ} {ψ : CNF ℕ} {u w : ℕ}
 
+/-- **The arcs of the graph of a formula**: those of the diamonds `j < xs.length`, the arc from the
+top of diamond `xs.length` to the chooser node, the arcs from the chooser node to the clause nodes,
+and the arcs from the node of clause `i` to the value node of `!b` in the diamond of the last
+quantifier over `x`, for each literal `(x, b)` of clause `i` with `x ∈ xs`. -/
 theorem mem_formulaArcs :
     (u, w) ∈ formulaArcs xs ψ ↔
       (∃ j < xs.length, (u = topNode j ∧ ∃ b, w = valueNode j b) ∨
diff --git a/Complexity/Computability/Complexity/Classes/TFNP.lean b/Complexity/Computability/Complexity/Classes/TFNP.lean
index cd2a7ae2b..d291fde8b 100644
--- a/Complexity/Computability/Complexity/Classes/TFNP.lean
+++ b/Complexity/Computability/Complexity/Classes/TFNP.lean
@@ -169,19 +169,19 @@ end Basic
 /-- The search problems in `FNP` with respect to the encoding `enc` of instances: relations that
 are polynomially balanced, every solution of `a` having length at most `p (enc a).length` for a
 polynomial `p`, and decided by a polynomial-time function of the instance and the candidate
-solution. -/
+solution [Papadimitriou, Section 10.3][Papadimitriou94]. -/
 def FNP (enc : α ↪ List Bool) : Set (α → List Bool → Prop) :=
   {R | (∃ p : Polynomial ℕ, ∀ a w, R a w → w.length ≤ p.eval (enc a).length) ∧
     ∃ V : α × List Bool → Bool, ComputableInPolyTime V (encPair enc encBits) encBool ∧
       ∀ a w, R a w ↔ V (a, w) = true}
 
 /-- The search problems in `FNP` solved by a polynomial-time function, Papadimitriou's class `FP`
-of search problems. -/
+of search problems [Papadimitriou, Section 10.3][Papadimitriou94]. -/
 def FPSearch (enc : α ↪ List Bool) : Set (α → List Bool → Prop) :=
   {R | R ∈ FNP enc ∧ ∃ f : α → Option (List Bool),
     ComputableInPolyTime f enc (encOption encBits) ∧ SolvesSearch R f}
 
-/-- The total search problems in `FNP`. -/
+/-- The total search problems in `FNP` [Megiddo and Papadimitriou][MegiddoPapadimitriou1991]. -/
 def TFNP (enc : α ↪ List Bool) : Set (α → List Bool → Prop) :=
   {R | R ∈ FNP enc ∧ IsTotalSearch R}
 
@@ -211,8 +211,10 @@ theorem mem_FPSearch_iff_tidy : R ∈ FPSearch enc ↔ R ∈ FNP enc ∧ ∃ f :
 
 theorem mem_TFNP : R ∈ TFNP enc ↔ R ∈ FNP enc ∧ IsTotalSearch R := Iff.rfl
 
+/-- Every search problem in `FPSearch` is in `FNP`. -/
 theorem FPSearch_subset_FNP : FPSearch enc ⊆ FNP enc := fun _ h => h.1
 
+/-- Every search problem in `TFNP` is in `FNP`. -/
 theorem TFNP_subset_FNP : TFNP enc ⊆ FNP enc := fun _ h => h.1
 
 /-- **`FNP` with the length bound in the verifier.** A relation is in `FNP` exactly when it holds
diff --git a/Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean b/Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean
index 0ebc999dc..f3486a61e 100644
--- a/Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean
+++ b/Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean
@@ -257,6 +257,7 @@ variables in order of first occurrence, that are no longer than the encoded form
 def searchRel (φ : Logic.PL.CNF ℕ) (w : List Bool) : Prop :=
   w.length ≤ (encCNF φ).length ∧ verifier (φ, w) = true
 
+/-- The search problem of `SAT` is in `FNP`. -/
 theorem searchRel_mem_FNP : searchRel ∈ FNP encCNF :=
   mem_FNP_iff_exists_bounded.2 ⟨Polynomial.X, verifier, computableTidilyInPolyTime_verifier,
     fun _ _ => by simp [searchRel]⟩
diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean
index 6c364ebd4..1dbee0271 100644
--- a/Complexity/Computability/Complexity/Classes/Time.lean
+++ b/Complexity/Computability/Complexity/Classes/Time.lean
@@ -151,7 +151,8 @@ private theorem exists_linear_of_eventually_le {t₁ t₂ : ℕ → ℕ} (h : 
 
 /-- The problems decidable within time `O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and
 `c₂`, on instances whose encoding under `enc` has length `n`, by a machine with a binary alphabet
-and finitely many states, with any space bound. -/
+and finitely many states, with any space bound
+[Arora and Barak, Definition 1.12][AroraBarak09]. -/
 def DTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
   {A | ∃ c₁ c₂ : ℕ, ∃ s : ℕ → ℕ,
     DecidableInTimeAndSpace A enc (fun a => c₁ * t (enc a).length + c₂) fun a => s (enc a).length}
@@ -265,7 +266,8 @@ end TimedReductions
 /-- The problems decidable within time `O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and
 `c₂`, on instances whose encoding under `enc` has length `n`, by a nondeterministic machine with a
 binary alphabet and finitely many states: every computation path of that many steps has halted,
-and `a ∈ A` exactly when some computation path halts with output `[true]`. -/
+and `a ∈ A` exactly when some computation path halts with output `[true]`
+[Arora and Barak, Definition 2.5][AroraBarak09]. -/
 def NTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
   {A | ∃ c₁ c₂ : ℕ, MultiTapeNTM.DecidableInTime A enc fun a => c₁ * t (enc a).length + c₂}
 
@@ -308,7 +310,8 @@ theorem DTIME_subset_NTIME {enc : α ↪ List Bool} {t : ℕ → ℕ} : DTIME en
 /-- The problems decidable with bounded error within time `O(t n)`, that is `c₁ * t n + c₂` for
 constants `c₁` and `c₂`, on instances whose encoding under `enc` has length `n`, by a fair-coin
 machine with a binary alphabet and finitely many states: every run of that many steps has halted,
-and outputs the right answer with probability at least `2 / 3`. -/
+and outputs the right answer with probability at least `2 / 3`
+[Arora and Barak, Definition 7.2][AroraBarak09]. -/
 def BPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
   {A | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State)
     (machine : MultiTapePTM k Bool State),
diff --git a/Complexity/Computability/Complexity/Classes/UP.lean b/Complexity/Computability/Complexity/Classes/UP.lean
index 4ac53ce25..509e6e291 100644
--- a/Complexity/Computability/Complexity/Classes/UP.lean
+++ b/Complexity/Computability/Complexity/Classes/UP.lean
@@ -47,7 +47,7 @@ open Turing.MultiTapeTM
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
 /-- Unambiguous polynomial time: some `#P` function is bounded by one everywhere and is one
-exactly on the language. -/
+exactly on the language [Papadimitriou][Papadimitriou94]. -/
 def UP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, (∀ a, f a ≤ 1) ∧ ∀ a, a ∈ A ↔ f a = 1}
 
diff --git a/Complexity/Computability/Complexity/Classes/US.lean b/Complexity/Computability/Complexity/Classes/US.lean
index 6ba373e79..8f6612b79 100644
--- a/Complexity/Computability/Complexity/Classes/US.lean
+++ b/Complexity/Computability/Complexity/Classes/US.lean
@@ -38,7 +38,8 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- Exactly one accepting witness, with no ambiguity restriction on no-instances. -/
+/-- Exactly one accepting witness, with no ambiguity restriction on no-instances
+[Blass and Gurevich][BlassGurevich1982]. -/
 def US (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, ∀ a, a ∈ A ↔ f a = 1}
 
diff --git a/Complexity/Computability/Complexity/Classes/WPP.lean b/Complexity/Computability/Complexity/Classes/WPP.lean
index 85dbc63cd..484d21f6e 100644
--- a/Complexity/Computability/Complexity/Classes/WPP.lean
+++ b/Complexity/Computability/Complexity/Classes/WPP.lean
@@ -81,12 +81,14 @@ open scoped symmDiff
 
 variable {α β : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- Wide gaps: zero on nonmembers and a nonzero binary FP target on members. -/
+/-- Wide gaps: zero on nonmembers and a nonzero binary FP target on members
+[Fenner, Fortnow and Kurtz][FennerFortnowKurtz1994]. -/
 def WPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ g ∈ GapP enc, ∃ f : α → ℤ, ComputableInPolyTime f enc encIntBin ∧
     (∀ a, f a ≠ 0) ∧ (∀ a, g a = 0 ∨ g a = f a) ∧ ∀ a, a ∈ A ↔ g a = f a}
 
-/-- Wide gaps with a target computed in polynomial time from unary input length. -/
+/-- Wide gaps with a target computed in polynomial time from unary input length
+[Fenner, Fortnow and Kurtz][FennerFortnowKurtz1994]. -/
 def LWPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ g ∈ GapP enc, ∃ f : ℕ → ℤ, ComputableInPolyTime f encUnary encIntBin ∧
     (∀ n, f n ≠ 0) ∧ (∀ a, g a = 0 ∨ g a = f (enc a).length) ∧
diff --git a/Complexity/Computability/Complexity/Classes/ZPP.lean b/Complexity/Computability/Complexity/Classes/ZPP.lean
index a33b2de80..6af7e59dd 100644
--- a/Complexity/Computability/Complexity/Classes/ZPP.lean
+++ b/Complexity/Computability/Complexity/Classes/ZPP.lean
@@ -51,6 +51,7 @@ the random strings, and on a non-member the second does.
 
 ## References
 
+* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
 -/
 
@@ -74,7 +75,8 @@ def DecidesWithZeroError (enc : α ↪ List Bool) (p : Polynomial ℕ)
         (V (a, List.ofFn r)).isSome = true).card
 
 /-- The problems decided with zero error by polynomial-time machines reading polynomially long
-random strings, with respect to the encoding `enc` of instances. -/
+random strings, with respect to the encoding `enc` of instances [Gill][Gill1977],
+[Arora and Barak, Section 7.3][AroraBarak09]. -/
 def ZPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Option Bool),
     ComputableInPolyTime V (encPair enc encBits) (encOption encBool) ∧
diff --git a/Complexity/Computability/Complexity/CookLevin/Correctness.lean b/Complexity/Computability/Complexity/CookLevin/Correctness.lean
index 86cfa30ad..8357ae26d 100644
--- a/Complexity/Computability/Complexity/CookLevin/Correctness.lean
+++ b/Complexity/Computability/Complexity/CookLevin/Correctness.lean
@@ -34,6 +34,10 @@ step equation.
 
 * `Cslib.Complexity.CookLevin.exists_eval_tableau_iff`: the tableau with fixed certificate bits.
 * `Cslib.Complexity.CookLevin.tableau_satisfiable_iff`: the tableau is correct.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09], Section 2.3.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/Complexity/Parameterized.lean b/Complexity/Computability/Complexity/Parameterized.lean
index 111d67f72..c2d625067 100644
--- a/Complexity/Computability/Complexity/Parameterized.lean
+++ b/Complexity/Computability/Complexity/Parameterized.lean
@@ -135,10 +135,14 @@ def XP (enc : α ↪ List Bool) (κ : α → ℕ) : Set (Set α) :=
 
 variable {enc : α ↪ List Bool} {κ κ' : α → ℕ} {A : Set α}
 
+/-- Membership in `FPT`: decidability within time `f (κ a) * (|enc a| + 1) ^ c` up to a constant
+factor, for some function `f` and constant `c`. -/
 theorem mem_FPT : A ∈ FPT enc κ ↔
     ∃ (f : ℕ → ℕ) (c : ℕ), DecidableInTimeO A enc fun a => f (κ a) * ((enc a).length + 1) ^ c :=
   Iff.rfl
 
+/-- Membership in `XP`: decidability within time `f (κ a) * (|enc a| + 1) ^ g (κ a)` up to a
+constant factor, for some functions `f` and `g`. -/
 theorem mem_XP : A ∈ XP enc κ ↔ ∃ f g : ℕ → ℕ,
     DecidableInTimeO A enc fun a => f (κ a) * ((enc a).length + 1) ^ g (κ a) :=
   Iff.rfl
diff --git a/Complexity/Computability/Complexity/Problems/CircuitSAT.lean b/Complexity/Computability/Complexity/Problems/CircuitSAT.lean
index b35b67d08..4c324c9ba 100644
--- a/Complexity/Computability/Complexity/Problems/CircuitSAT.lean
+++ b/Complexity/Computability/Complexity/Problems/CircuitSAT.lean
@@ -64,7 +64,7 @@ namespace Cslib.Complexity
 open Circuits Circuits.Boolean Turing.MultiTapeTM Cslib.Logic.PL
 
 /-- **Circuit satisfiability**: the De Morgan circuits with one output that output true on some
-input. -/
+input [Arora and Barak, Section 6.1][AroraBarak09]. -/
 def CircuitSAT : Set (Σ n, Circuit signature n 1) :=
   {c | ∃ x : BitString c.1, c.2.eval interpretation x 0 = true}
 
@@ -425,7 +425,7 @@ theorem CircuitSAT_npHard : NPHard (encCircuit 1) CircuitSAT :=
   CookLevin.SAT_npHard.trans SAT.polyTimeReducible_CircuitSAT
 
 /-- **Circuit satisfiability is `NP`-complete**, for the binary encoding of circuits
-`encCircuit 1`. -/
+`encCircuit 1` [Arora and Barak, Section 6.1][AroraBarak09]. -/
 theorem CircuitSAT_npComplete : NPComplete (encCircuit 1) CircuitSAT :=
   ⟨CircuitSAT.mem_NP, CircuitSAT_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/Coloring.lean b/Complexity/Computability/Complexity/Problems/Coloring.lean
index c5610687d..64ab49648 100644
--- a/Complexity/Computability/Complexity/Problems/Coloring.lean
+++ b/Complexity/Computability/Complexity/Problems/Coloring.lean
@@ -83,11 +83,11 @@ namespace Cslib.Complexity
 open Cslib.Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime
 
 /-- The graphs whose declared vertices can be colored with `k` colors, adjacent vertices getting
-different colors. -/
+different colors [Karp1972]. -/
 def KColoring (k : ℕ) : Set Graph := {G | (G.toSimpleGraph.induce {v | v ∈ G.1}).Colorable k}
 
 /-- The graphs whose declared vertices can be colored with three colors, adjacent vertices getting
-different colors. -/
+different colors [Sipser, Chapter 7][Sipser2013]. -/
 abbrev ThreeColoring : Set Graph := KColoring 3
 
 /-- Membership in `KColoring k` as a coloring by natural numbers below `k`. -/
@@ -758,7 +758,7 @@ theorem polyTimeReducible_ThreeSAT_ThreeColoring :
 theorem ThreeColoring_npHard : NPHard encGraph ThreeColoring :=
   CookLevin.SAT_npHard.trans polyTimeReducible_SAT_ThreeColoring
 
-/-- **`ThreeColoring` is NP-complete.** -/
+/-- **`ThreeColoring` is NP-complete** [Garey and Johnson][GareyJohnson1979]. -/
 theorem ThreeColoring_npComplete : NPComplete encGraph ThreeColoring :=
   ⟨KColoring.mem_NP 3, ThreeColoring_npHard⟩
 
@@ -774,7 +774,7 @@ theorem polyTimeReducible_SAT_KColoring {k : ℕ} (hk : 3 ≤ k) :
 theorem KColoring_npHard {k : ℕ} (hk : 3 ≤ k) : NPHard encGraph (KColoring k) :=
   CookLevin.SAT_npHard.trans (polyTimeReducible_SAT_KColoring hk)
 
-/-- **For `k ≥ 3`, `KColoring k` is NP-complete.** -/
+/-- **For `k ≥ 3`, `KColoring k` is NP-complete** [Garey and Johnson][GareyJohnson1979]. -/
 theorem KColoring_npComplete {k : ℕ} (hk : 3 ≤ k) : NPComplete encGraph (KColoring k) :=
   ⟨KColoring.mem_NP k, KColoring_npHard hk⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/ExactThreeSAT.lean b/Complexity/Computability/Complexity/Problems/ExactThreeSAT.lean
index 8cbd9f9f3..3626e0286 100644
--- a/Complexity/Computability/Complexity/Problems/ExactThreeSAT.lean
+++ b/Complexity/Computability/Complexity/Problems/ExactThreeSAT.lean
@@ -54,7 +54,8 @@ namespace Cslib.Complexity
 open Cslib.Logic.PL Turing.MultiTapeTM
 
 /-- The satisfiable formulas all of whose clauses have exactly three literals, not necessarily
-distinct. -/
+distinct. The 3-satisfiability of [Garey and Johnson, Problem LO2][GareyJohnson1979] requires
+them to be distinct. -/
 def ExactThreeSAT : Set (CNF ℕ) := {φ | (∀ c ∈ φ, c.length = 3) ∧ φ.Satisfiable}
 
 namespace ExactThreeSAT
diff --git a/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean b/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean
index 761638c5c..4b656365f 100644
--- a/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean
+++ b/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean
@@ -93,10 +93,11 @@ theorem computableTidilyInPolyTime_adjIndex {γ : Type} {input : γ ↪ List Boo
 
 end Graph
 
-/-- The pairs of isomorphic graphs: the graphs induced on the declared vertices are isomorphic. -/
+/-- The pairs of isomorphic graphs: the graphs induced on the declared vertices are isomorphic
+[Arora and Barak, Section 8.1.3][AroraBarak09]. -/
 def GraphIsomorphism : Set (Graph × Graph) := {x | Nonempty (x.1.induced ≃g x.2.induced)}
 
-/-- The pairs of non-isomorphic graphs. -/
+/-- The pairs of non-isomorphic graphs [Arora and Barak, Section 8.1.3][AroraBarak09]. -/
 def GraphNonIsomorphism : Set (Graph × Graph) := GraphIsomorphismᶜ
 
 /-- Two graphs are isomorphic exactly when a bijection between the positions of their distinct
diff --git a/Complexity/Computability/Complexity/Problems/Hamiltonian.lean b/Complexity/Computability/Complexity/Problems/Hamiltonian.lean
index b73805936..5adaa934a 100644
--- a/Complexity/Computability/Complexity/Problems/Hamiltonian.lean
+++ b/Complexity/Computability/Complexity/Problems/Hamiltonian.lean
@@ -104,19 +104,21 @@ def IsDirHamCycle (G : Graph) (p : List ℕ) : Prop :=
 
 end Graph
 
-/-- The directed graphs with a Hamiltonian path from `s` to `t`. -/
+/-- The directed graphs with a Hamiltonian path from `s` to `t`
+[Sipser, Section 7.3][Sipser2013]. -/
 def DirHamPath : Set (Graph × ℕ × ℕ) := {x | ∃ p, x.1.IsDirHamPath x.2.1 x.2.2 p}
 
-/-- The directed graphs with a Hamiltonian cycle. -/
+/-- The directed graphs with a Hamiltonian cycle [Karp1972]. -/
 def DirHamCycle : Set Graph := {G | ∃ p, G.IsDirHamCycle p}
 
-/-- The graphs with a Hamiltonian path from `s` to `t` through their declared vertices. -/
+/-- The graphs with a Hamiltonian path from `s` to `t` through their declared vertices
+[Sipser, Theorem 7.55][Sipser2013]. -/
 def HamPath : Set (Graph × ℕ × ℕ) :=
   {x | ∃ (hs : x.2.1 ∈ x.1.1) (ht : x.2.2 ∈ x.1.1)
     (p : (x.1.toSimpleGraph.induce {v | v ∈ x.1.1}).Walk ⟨x.2.1, hs⟩ ⟨x.2.2, ht⟩),
     p.IsHamiltonian}
 
-/-- The graphs with a Hamiltonian cycle through their declared vertices. -/
+/-- The graphs with a Hamiltonian cycle through their declared vertices [Karp1972]. -/
 def HamCycle : Set Graph :=
   {G | ∃ (a : {v | v ∈ G.1}) (p : (G.toSimpleGraph.induce {v | v ∈ G.1}).Walk a a),
     p.IsHamiltonianCycle}
diff --git a/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean b/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean
index c88f5a145..efc0b5c61 100644
--- a/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean
+++ b/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean
@@ -588,7 +588,7 @@ theorem polyTimeReducible_DirHamCycle_HamCycle :
 theorem HamPath_npHard : NPHard (encPair encGraph (encPair encNat encNat)) HamPath :=
   DirHamPath_npHard.trans polyTimeReducible_DirHamPath_HamPath
 
-/-- **`HamPath` is NP-complete.** -/
+/-- **`HamPath` is NP-complete** [Sipser, Theorem 7.55][Sipser2013]. -/
 theorem HamPath_npComplete : NPComplete (encPair encGraph (encPair encNat encNat)) HamPath :=
   ⟨HamPath.mem_NP, HamPath_npHard⟩
 
@@ -596,7 +596,7 @@ theorem HamPath_npComplete : NPComplete (encPair encGraph (encPair encNat encNat
 theorem HamCycle_npHard : NPHard encGraph HamCycle :=
   DirHamCycle_npHard.trans polyTimeReducible_DirHamCycle_HamCycle
 
-/-- **`HamCycle` is NP-complete.** -/
+/-- **`HamCycle` is NP-complete** [Karp1972]. -/
 theorem HamCycle_npComplete : NPComplete encGraph HamCycle :=
   ⟨HamCycle.mem_NP, HamCycle_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/IndependentSet.lean b/Complexity/Computability/Complexity/Problems/IndependentSet.lean
index d5b2d197b..8a413fdee 100644
--- a/Complexity/Computability/Complexity/Problems/IndependentSet.lean
+++ b/Complexity/Computability/Complexity/Problems/IndependentSet.lean
@@ -87,7 +87,8 @@ def encGraph : Graph ↪ List Bool :=
 in either direction. -/
 def Graph.toSimpleGraph (G : Graph) : SimpleGraph ℕ := SimpleGraph.fromRel fun u v => (u, v) ∈ G.2
 
-/-- The graphs with an independent set of `m` of their vertices. -/
+/-- The graphs with an independent set of `m` of their vertices
+[Arora and Barak, Section 2.4][AroraBarak09]. -/
 def IndependentSet : Set (Graph × ℕ) :=
   {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ x.1.toSimpleGraph.IsNIndepSet x.2 S}
 
@@ -501,7 +502,7 @@ theorem polyTimeReducible_SAT_IndependentSet :
 theorem IndependentSet_npHard : NPHard (encPair encGraph encNat) IndependentSet :=
   CookLevin.SAT_npHard.trans polyTimeReducible_SAT_IndependentSet
 
-/-- **`IndependentSet` is NP-complete.** -/
+/-- **`IndependentSet` is NP-complete** [Arora and Barak, Section 2.4][AroraBarak09]. -/
 theorem IndependentSet_npComplete : NPComplete (encPair encGraph encNat) IndependentSet :=
   ⟨IndependentSet.mem_NP, IndependentSet_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/IntegerProgramming.lean b/Complexity/Computability/Complexity/Problems/IntegerProgramming.lean
index 271415929..bedc314f4 100644
--- a/Complexity/Computability/Complexity/Problems/IntegerProgramming.lean
+++ b/Complexity/Computability/Complexity/Problems/IntegerProgramming.lean
@@ -49,8 +49,9 @@ namespace Cslib.Complexity
 
 open Finset Turing.MultiTapeTM ComputableTidilyInPolyTime
 
-/-- The systems of linear equations with natural coefficients that have a zero-one solution. A
-constraint `(a, t)` asks for `∑ j < a.length, a[j] * x j = t`. -/
+/-- The systems of linear equations with natural coefficients that have a zero-one solution, the
+equality form of Karp's zero-one integer programming [Karp1972]. A constraint `(a, t)` asks for
+`∑ j < a.length, a[j] * x j = t`. -/
 def ZeroOneIP : Set (List (List ℕ × ℕ)) :=
   {C | ∃ x : ℕ → Bool, ∀ c ∈ C, ∑ j ∈ range c.1.length, c.1.getD j 0 * (x j).toNat = c.2}
 
@@ -152,7 +153,7 @@ theorem ZeroOneIP_npHard : NPHard (encList (encPair (encList encNat) encNat)) Ze
   ThreeSAT_npHard.trans polyTimeReducible_ThreeSAT_ZeroOneIP
 
 /-- **Zero-one integer programming is NP-complete**, in equality form with natural coefficients
-in binary. -/
+in binary [Karp1972]. -/
 theorem ZeroOneIP_npComplete : NPComplete (encList (encPair (encList encNat) encNat)) ZeroOneIP :=
   ⟨ZeroOneIP.mem_NP, ZeroOneIP_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/Knapsack.lean b/Complexity/Computability/Complexity/Problems/Knapsack.lean
index 4a07dc84f..52447bae8 100644
--- a/Complexity/Computability/Complexity/Problems/Knapsack.lean
+++ b/Complexity/Computability/Complexity/Problems/Knapsack.lean
@@ -16,11 +16,12 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na
 
 `Knapsack` is the decision version of the 0-1 knapsack problem: given items, each with a weight
 and a value, a capacity and a goal, some sub-multiset of the items has total weight at most the
-capacity and total value at least the goal [Karp1972]. All numbers are encoded in binary
+capacity and total value at least the goal [GareyJohnson1979]. All numbers are encoded in binary
 (`encNat`); the verifier compares the sums in binary (`ComputableTidilyInPolyTime.binary_le`).
 
 Giving every number of a subset sum instance equal weight and value, and taking the target as
-both capacity and goal, reduces `SubsetSum` to `Knapsack`.
+both capacity and goal, reduces `SubsetSum` to `Knapsack`. Karp's KNAPSACK [Karp1972] is the
+subset sum form of the problem.
 
 ## Main definitions
 
@@ -39,6 +40,7 @@ both capacity and goal, reduces `SubsetSum` to `Knapsack`.
 ## References
 
 * [R. M. Karp, *Reducibility among combinatorial problems*][Karp1972]
+* [M. R. Garey and D. S. Johnson, *Computers and Intractability*][GareyJohnson1979]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
 -/
 
@@ -51,7 +53,7 @@ open scoped List
 
 /-- Instances `(items, capacity, goal)` of the 0-1 knapsack problem, items given as
 `(weight, value)`: some sub-multiset of the items has total weight at most the capacity and total
-value at least the goal. -/
+value at least the goal [Garey and Johnson][GareyJohnson1979]. -/
 def Knapsack : Set (List (ℕ × ℕ) × ℕ × ℕ) :=
   {x | ∃ s ≤ (x.1 : Multiset (ℕ × ℕ)),
     (s.map Prod.fst).sum ≤ x.2.1 ∧ x.2.2 ≤ (s.map Prod.snd).sum}
@@ -137,7 +139,8 @@ theorem polyTimeReducible_SubsetSum_Knapsack :
 theorem Knapsack_npHard : NPHard encKnapsack Knapsack :=
   SubsetSum_npHard.trans polyTimeReducible_SubsetSum_Knapsack
 
-/-- **The 0-1 knapsack problem is NP-complete**, with all numbers in binary. -/
+/-- **The 0-1 knapsack problem is NP-complete**, with all numbers in binary
+[Garey and Johnson][GareyJohnson1979]. -/
 theorem Knapsack_npComplete : NPComplete encKnapsack Knapsack :=
   ⟨Knapsack.mem_NP, Knapsack_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue.lean b/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue.lean
index 1f3dcef6e..1f1439bf0 100644
--- a/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue.lean
+++ b/Complexity/Computability/Complexity/Problems/MonotoneCircuitValue.lean
@@ -59,7 +59,7 @@ namespace Cslib.Complexity
 open Circuits Circuits.Boolean Turing.MultiTapeTM
 
 /-- **The monotone circuit value problem**: the monotone circuits with one output, each with an
-input of its arity, whose output on that input is true. -/
+input of its arity, whose output on that input is true [Goldschlager1977]. -/
 def MonotoneCircuitValue : Set (Σ n, Circuit Monotone.signature n 1 × BitString n) :=
   {x | x.2.1.eval Monotone.interpretation x.2.2 0 = true}
 
diff --git a/Complexity/Computability/Complexity/Problems/Partition.lean b/Complexity/Computability/Complexity/Problems/Partition.lean
index afc030f8f..049e8c727 100644
--- a/Complexity/Computability/Complexity/Problems/Partition.lean
+++ b/Complexity/Computability/Complexity/Problems/Partition.lean
@@ -52,7 +52,7 @@ namespace Cslib.Complexity
 open Turing.MultiTapeTM ComputableTidilyInPolyTime
 open scoped List
 
-/-- The lists of natural numbers that split into two sub-multisets with equal sums. -/
+/-- The lists of natural numbers that split into two sub-multisets with equal sums [Karp1972]. -/
 def Partition : Set (List ℕ) := {l | ∃ s t : Multiset ℕ, s + t = l ∧ s.sum = t.sum}
 
 /-- A partition is a sub-multiset holding half of the total sum. -/
@@ -152,7 +152,7 @@ theorem polyTimeReducible_SubsetSum_Partition :
 theorem Partition_npHard : NPHard (encList encNat) Partition :=
   SubsetSum_npHard.trans polyTimeReducible_SubsetSum_Partition
 
-/-- **Partition is NP-complete**, with the numbers in binary. -/
+/-- **Partition is NP-complete**, with the numbers in binary [Karp1972]. -/
 theorem Partition_npComplete : NPComplete (encList encNat) Partition :=
   ⟨Partition.mem_NP, Partition_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/SAT.lean b/Complexity/Computability/Complexity/Problems/SAT.lean
index c674e7f0f..8c741dd34 100644
--- a/Complexity/Computability/Complexity/Problems/SAT.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT.lean
@@ -40,6 +40,7 @@ reduction and `NP`-completeness are proved in `CookLevin/`.
 
 ## References
 
+* [R. M. Karp, *Reducibility among combinatorial problems*][Karp1972]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
 -/
 
@@ -49,7 +50,8 @@ namespace Cslib.Complexity
 
 open Cslib.Logic.PL Turing.MultiTapeTM
 
-/-- The satisfiable CNF formulas over variables numbered by natural numbers. -/
+/-- The satisfiable CNF formulas over variables numbered by natural numbers [Karp1972],
+[Arora and Barak, Section 2.3][AroraBarak09]. -/
 def SAT : Set (CNF ℕ) := {φ | φ.Satisfiable}
 
 theorem mem_SAT {φ : CNF ℕ} : φ ∈ SAT ↔ φ.Satisfiable := Iff.rfl
diff --git a/Complexity/Computability/Complexity/Problems/SATUNSAT.lean b/Complexity/Computability/Complexity/Problems/SATUNSAT.lean
index a805160bb..4af5f8de4 100644
--- a/Complexity/Computability/Complexity/Problems/SATUNSAT.lean
+++ b/Complexity/Computability/Complexity/Problems/SATUNSAT.lean
@@ -33,7 +33,8 @@ namespace Cslib.Complexity
 
 open Turing.MultiTapeTM Cslib.Logic.PL
 
-/-- Pairs of a satisfiable CNF formula and an unsatisfiable CNF formula. -/
+/-- Pairs of a satisfiable CNF formula and an unsatisfiable CNF formula
+[Papadimitriou, Chapter 17][Papadimitriou94]. -/
 def SATUNSAT : Set (CNF ℕ × CNF ℕ) := SAT ×ˢ UNSAT
 
 /-- SAT–UNSAT is DP-complete with the product of the library's CNF encodings. -/
diff --git a/Complexity/Computability/Complexity/Problems/SubsetSum.lean b/Complexity/Computability/Complexity/Problems/SubsetSum.lean
index 28f8ee41b..b88944351 100644
--- a/Complexity/Computability/Complexity/Problems/SubsetSum.lean
+++ b/Complexity/Computability/Complexity/Problems/SubsetSum.lean
@@ -21,7 +21,7 @@ import Complexity.Logics.Propositional.CNF.PolyTime
 
 `SubsetSum` is the set of pairs `(a, t)` of a list `a` of natural numbers, possibly with
 repetitions, and a target `t` such that some sub-multiset of `a` sums to `t` [Sipser, Section
-7.4][Sipser2013]. All numbers are encoded in binary (`Turing.MultiTapeTM.encNat`, digits least
+7.3][Sipser2013]. All numbers are encoded in binary (`Turing.MultiTapeTM.encNat`, digits least
 significant first); the `NP`-hardness proved here is for this encoding and is not strong
 `NP`-hardness. A certificate is a mask selecting entries of `a` (`Cslib.Complexity.maskSelect`),
 and the verifier adds the selected numbers in binary.
@@ -77,7 +77,8 @@ namespace Cslib.Complexity
 open Cslib.Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime
 open scoped List
 
-/-- The instances `(a, t)` of subset sum: some sub-multiset of the numbers `a` sums to `t`. -/
+/-- The instances `(a, t)` of subset sum: some sub-multiset of the numbers `a` sums to `t`
+[Karp1972], [Sipser, Chapter 7][Sipser2013]. -/
 def SubsetSum : Set (List ℕ × ℕ) := {x | ∃ s ≤ (x.1 : Multiset ℕ), s.sum = x.2}
 
 theorem mem_SubsetSum {x : List ℕ × ℕ} :
@@ -675,7 +676,8 @@ theorem polyTimeReducible_ThreeSAT_SubsetSum :
 theorem SubsetSum_npHard : NPHard (encPair (encList encNat) encNat) SubsetSum :=
   ThreeSAT_npHard.trans polyTimeReducible_ThreeSAT_SubsetSum
 
-/-- **Subset sum is NP-complete**, with the numbers and the target in binary. -/
+/-- **Subset sum is NP-complete**, with the numbers and the target in binary [Karp1972],
+[Sipser, Theorem 7.56][Sipser2013]. -/
 theorem SubsetSum_npComplete : NPComplete (encPair (encList encNat) encNat) SubsetSum :=
   ⟨SubsetSum.mem_NP, SubsetSum_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean b/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean
index c54396025..a78dd9073 100644
--- a/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean
+++ b/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean
@@ -62,6 +62,7 @@ theorem maskSelect_cons (a : α) (l : List α) (w : List Bool) :
   | nil => simp
   | cons b w => cases b <;> simp [List.map_map, Function.comp_def]
 
+/-- A mask selects a sublist. -/
 theorem maskSelect_sublist (l : List α) (w : List Bool) : maskSelect l w <+ l := by
   simpa only [maskSelect, List.zipIdx_map_fst] using
     (List.filter_sublist (p := fun p : α × ℕ => w.getD p.2 false) (l := l.zipIdx)).map Prod.fst
diff --git a/Complexity/Computability/Complexity/Problems/TQBF.lean b/Complexity/Computability/Complexity/Problems/TQBF.lean
index b32bf54a3..f8732d2b0 100644
--- a/Complexity/Computability/Complexity/Problems/TQBF.lean
+++ b/Complexity/Computability/Complexity/Problems/TQBF.lean
@@ -193,6 +193,7 @@ def encQBF : QBF ℕ ↪ List Bool :=
   ⟨fun φ => encList TQBF.encToken φ.tokens,
     fun _ _ h => QBF.tokens_injective ((encList TQBF.encToken).injective h)⟩
 
+/-- A formula is encoded as the list of its framed tokens in prefix order. -/
 theorem encQBF_apply (φ : QBF ℕ) : encQBF φ = encList TQBF.encToken φ.tokens := rfl
 
 /-- Every node takes at least three bits. -/
@@ -207,9 +208,12 @@ theorem three_mul_length_tokens_le (φ : QBF ℕ) : 3 * φ.tokens.length ≤ (en
 
 /-! ### True closed formulas -/
 
-/-- **The true closed quantified Boolean formulas** over variables numbered by natural numbers. -/
+/-- **The true closed quantified Boolean formulas** over variables numbered by natural numbers
+[Sipser, Section 8.3][Sipser2013], [Arora and Barak, Section 4.2][AroraBarak09]. -/
 def TQBF : Set (QBF ℕ) := {φ | φ.Closed ∧ φ.eval (fun _ => false) = true}
 
+/-- A formula is in `TQBF` exactly when it is closed and true under the assignment
+`fun _ => false`. -/
 theorem mem_TQBF {φ : QBF ℕ} : φ ∈ TQBF ↔ φ.Closed ∧ φ.eval (fun _ => false) = true := Iff.rfl
 
 /-- A closed formula is in `TQBF` exactly when it is true under some, equivalently every,
diff --git a/Complexity/Computability/Complexity/Problems/TSP.lean b/Complexity/Computability/Complexity/Problems/TSP.lean
index 8b07fbb53..a1f72edf2 100644
--- a/Complexity/Computability/Complexity/Problems/TSP.lean
+++ b/Complexity/Computability/Complexity/Problems/TSP.lean
@@ -96,7 +96,8 @@ def tourLength (D : List (List ℕ)) (p : List ℕ) : ℕ :=
 end TSP
 
 /-- The traveling salesman problem: the distance matrices `D` with a budget `b` such that some
-closed tour visiting each city `0, …, D.length - 1` exactly once has length at most `b`. -/
+closed tour visiting each city `0, …, D.length - 1` exactly once has length at most `b`
+[Papadimitriou, Section 9.3][Papadimitriou94]. -/
 def TSP : Set (List (List ℕ) × ℕ) :=
   {x | ∃ p : List ℕ, p.Perm (List.range x.1.length) ∧ TSP.tourLength x.1 p ≤ x.2}
 
@@ -411,7 +412,7 @@ theorem polyTimeReducible_HamCycle_TSP : PolyTimeReducible encGraph encTSP HamCy
 theorem TSP_npHard : NPHard encTSP TSP :=
   HamCycle_npHard.trans polyTimeReducible_HamCycle_TSP
 
-/-- `TSP` is `NP`-complete. -/
+/-- **`TSP` is NP-complete** [Papadimitriou, Section 9.3][Papadimitriou94]. -/
 theorem TSP_npComplete : NPComplete encTSP TSP :=
   ⟨TSP.mem_NP, TSP_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/ThreeSAT.lean b/Complexity/Computability/Complexity/Problems/ThreeSAT.lean
index a20444092..5faea60b2 100644
--- a/Complexity/Computability/Complexity/Problems/ThreeSAT.lean
+++ b/Complexity/Computability/Complexity/Problems/ThreeSAT.lean
@@ -44,6 +44,7 @@ relabelling and the Cook–Levin theorem proves that `ThreeSAT` is `NP`-complete
 
 ## References
 
+* [R. M. Karp, *Reducibility among combinatorial problems*][Karp1972]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
 -/
 
@@ -53,7 +54,8 @@ namespace Cslib.Complexity
 
 open Cslib.Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime
 
-/-- The satisfiable formulas whose clauses have at most three literals. -/
+/-- The satisfiable formulas whose clauses have at most three literals [Karp1972],
+[Arora and Barak, Section 2.3.1][AroraBarak09]. -/
 def ThreeSAT : Set (CNF ℕ) := {φ | (∀ c ∈ φ, c.length ≤ 3) ∧ φ.Satisfiable}
 
 /-- An injective numbering of the variables of a split formula: original variables at even
@@ -74,6 +76,8 @@ theorem splitVarToNat_injective : Function.Injective splitVarToNat := by
 /-- The reduction from `SAT` to `ThreeSAT`: split the clauses, then number the variables. -/
 def toThreeSAT (φ : CNF ℕ) : CNF ℕ := φ.to3CNF.relabel splitVarToNat
 
+/-- **Correctness of the reduction**: `toThreeSAT φ` is in `ThreeSAT` exactly when `φ` is in
+`SAT`. -/
 theorem mem_ThreeSAT_toThreeSAT_iff (φ : CNF ℕ) : toThreeSAT φ ∈ ThreeSAT ↔ φ ∈ SAT := by
   refine ⟨fun h => ?_, fun h => ⟨fun c hc => ?_, ?_⟩⟩
   · exact (CNF.satisfiable_to3CNF φ).1 ((CNF.satisfiable_relabel splitVarToNat_injective _).1 h.2)
@@ -194,7 +198,7 @@ theorem polyTimeReducible_SAT_ThreeSAT : PolyTimeReducible encCNF encCNF SAT Thr
 theorem ThreeSAT_npHard : NPHard encCNF ThreeSAT :=
   CookLevin.SAT_npHard.trans polyTimeReducible_SAT_ThreeSAT
 
-/-- **3SAT is NP-complete.** -/
+/-- **3SAT is NP-complete** [Karp1972]. -/
 theorem ThreeSAT_npComplete : NPComplete encCNF ThreeSAT :=
   ⟨ThreeSAT.mem_NP, ThreeSAT_npHard⟩
 
diff --git a/Complexity/Computability/Complexity/Problems/USAT.lean b/Complexity/Computability/Complexity/Problems/USAT.lean
index 27f1b6fd2..b0ac3ac5b 100644
--- a/Complexity/Computability/Complexity/Problems/USAT.lean
+++ b/Complexity/Computability/Complexity/Problems/USAT.lean
@@ -43,6 +43,7 @@ deciding either `USAT` or `SAT` does (`solvedBy_USAT`, `solvedBy_SAT`). `Promise
 
 ## References
 
+* [A. Blass, Y. Gurevich, *On the unique satisfiability problem*][BlassGurevich1982]
 * [L. G. Valiant, V. V. Vazirani, *NP is as easy as detecting unique
   solutions*][ValiantVazirani1986]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
@@ -55,7 +56,8 @@ namespace Cslib.Complexity
 open Cslib.Logic.PL PromiseProblem
 
 /-- The uniquely satisfiable formulas: some assignment satisfies the formula, and every satisfying
-assignment agrees with it on every variable of the formula. -/
+assignment agrees with it on every variable of the formula
+[Blass and Gurevich][BlassGurevich1982]. -/
 def USAT : Set (CNF ℕ) :=
   {φ | ∃ σ : ℕ → Bool, φ.eval σ = true ∧
     ∀ τ : ℕ → Bool, φ.eval τ = true → ∀ v ∈ φ.vars, τ v = σ v}
diff --git a/Complexity/Computability/Complexity/Problems/USTCON.lean b/Complexity/Computability/Complexity/Problems/USTCON.lean
index 530c79634..eb1afb61b 100644
--- a/Complexity/Computability/Complexity/Problems/USTCON.lean
+++ b/Complexity/Computability/Complexity/Problems/USTCON.lean
@@ -213,7 +213,8 @@ end USTCONInstance
 def encUSTCON : USTCONInstance ↪ List Bool :=
   ⟨USTCONInstance.encode, USTCONInstance.encode_injective⟩
 
-/-- **Undirected `s`–`t` connectivity**: the instances in which `t` is reachable from `s`. -/
+/-- **Undirected `s`–`t` connectivity**: the instances in which `t` is reachable from `s`
+[Arora and Barak, Section 21.4][AroraBarak09], [Reingold][Reingold2008]. -/
 def USTCON : Set USTCONInstance :=
   {I | I.graph.Reachable I.s I.t}
 
diff --git a/Complexity/Computability/Complexity/Problems/VertexCover.lean b/Complexity/Computability/Complexity/Problems/VertexCover.lean
index f96a6d10c..f9a569187 100644
--- a/Complexity/Computability/Complexity/Problems/VertexCover.lean
+++ b/Complexity/Computability/Complexity/Problems/VertexCover.lean
@@ -77,7 +77,7 @@ namespace Cslib.Complexity
 open Turing.MultiTapeTM ComputableTidilyInPolyTime
 
 /-- The graphs with a vertex cover of `k` of their vertices: `k` declared vertices meeting every
-edge between two declared vertices. -/
+edge between two declared vertices [Karp1972]. -/
 def VertexCover : Set (Graph × ℕ) :=
   {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧
     (x.1.toSimpleGraph.induce {v | v ∈ x.1.1}).IsVertexCover {v | ↑v ∈ S} ∧ S.card = x.2}
@@ -251,7 +251,7 @@ theorem polyTimeReducible_IndependentSet_VertexCover :
 theorem VertexCover_npHard : NPHard (encPair encGraph encNat) VertexCover :=
   IndependentSet_npHard.trans polyTimeReducible_IndependentSet_VertexCover
 
-/-- **`VertexCover` is NP-complete.** -/
+/-- **`VertexCover` is NP-complete** [Karp1972]. -/
 theorem VertexCover_npComplete : NPComplete (encPair encGraph encNat) VertexCover :=
   ⟨VertexCover.mem_NP, VertexCover_npHard⟩
 
diff --git a/Complexity/Computability/Kolmogorov/Basic.lean b/Complexity/Computability/Kolmogorov/Basic.lean
index aeddab88b..20f6658f6 100644
--- a/Complexity/Computability/Kolmogorov/Basic.lean
+++ b/Complexity/Computability/Kolmogorov/Basic.lean
@@ -295,6 +295,8 @@ theorem map_produces_iff {f : α → β} {M : DescriptionMethod α} {p : List Bo
   simp only [produces_iff_exists_mem_runFor, mem_map_runFor_iff]
   exact ⟨fun ⟨t, x, hx, hy⟩ => ⟨x, ⟨t, hx⟩, hy⟩, fun ⟨x, ⟨t, hx⟩, hy⟩ => ⟨t, x, hx, hy⟩⟩
 
+/-- Mapping `f` over the outputs does not increase complexity: `f x` has complexity under
+`M.map f` at most that of `x` under `M`. -/
 theorem ecomplexity_map_le (f : α → β) (M : DescriptionMethod α) (x : α) :
     (M.map f).ecomplexity (f x) ≤ M.ecomplexity x :=
   le_iInf₂ fun _ hp => ecomplexity_le_length (map_produces_iff.mpr ⟨x, hp, rfl⟩)
@@ -303,6 +305,8 @@ theorem etimeBoundedComplexity_map_le (f : α → β) (M : DescriptionMethod α)
     (M.map f).etimeBoundedComplexity t (f x) ≤ M.etimeBoundedComplexity t x :=
   le_iInf₂ fun _ hp => etimeBoundedComplexity_le_length (mem_map_runFor_iff.mpr ⟨x, hp, rfl⟩)
 
+/-- Mapping an injective `f` over the outputs preserves complexity: `f x` has the same
+complexity under `M.map f` as `x` under `M`. -/
 theorem ecomplexity_map_eq_of_injective {f : α → β} (hf : Function.Injective f)
     (M : DescriptionMethod α) (x : α) :
     (M.map f).ecomplexity (f x) = M.ecomplexity x :=
diff --git a/Complexity/Computability/Kolmogorov/SelfDelimiting.lean b/Complexity/Computability/Kolmogorov/SelfDelimiting.lean
index 9c2d7ea8d..fc23c400a 100644
--- a/Complexity/Computability/Kolmogorov/SelfDelimiting.lean
+++ b/Complexity/Computability/Kolmogorov/SelfDelimiting.lean
@@ -63,6 +63,7 @@ def decodeSelfDelimiting (q : List Bool) : List Bool × List Bool :=
   ((r.drop k).take n, (r.drop k).drop n)
 
 
+/-- The decoder inverts the code: it splits `selfDelimitingCode p ++ q` back into `p` and `q`. -/
 @[simp]
 theorem decodeSelfDelimiting_selfDelimitingCode_append (p q : List Bool) :
     decodeSelfDelimiting (selfDelimitingCode p ++ q) = (p, q) := by
diff --git a/Complexity/Computability/Languages/Slice.lean b/Complexity/Computability/Languages/Slice.lean
index f5281aa29..a225b70a7 100644
--- a/Complexity/Computability/Languages/Slice.lean
+++ b/Complexity/Computability/Languages/Slice.lean
@@ -30,23 +30,29 @@ namespace Language
 
 variable {α : Type*} {L M : Language α} {n : ℕ} {x : Fin n → α}
 
+/-- The slices of the empty language `0` are `false` everywhere. -/
 @[simp] theorem slice_zero : (0 : Language α).slice n x = false :=
   Bool.eq_false_iff.2 fun h => notMem_zero _ (slice_eq_true_iff.1 h)
 
+/-- The slices of the empty language `⊥` are `false` everywhere. -/
 @[simp] theorem slice_bot : (⊥ : Language α).slice n x = false :=
   slice_zero
 
+/-- The slices of the full language `⊤` are `true` everywhere. -/
 @[simp] theorem slice_top : (⊤ : Language α).slice n x = true := slice_eq_true_iff.2 trivial
 
+/-- The slice of a complement is the negation of the slice. -/
 @[simp] theorem slice_compl : Lᶜ.slice n x = !L.slice n x := by
   cases h : L.slice n x
   · exact slice_eq_true_iff.2 fun hm => by simp [slice_eq_true_iff.2 hm] at h
   · exact Bool.eq_false_iff.2 fun h' => (slice_eq_true_iff.1 h') (slice_eq_true_iff.1 h)
 
+/-- The slice of a union is the disjunction of the slices. -/
 @[simp] theorem slice_sup : (L ⊔ M).slice n x = (L.slice n x || M.slice n x) := by
   rw [Bool.eq_iff_iff, Bool.or_eq_true, slice_eq_true_iff, slice_eq_true_iff, slice_eq_true_iff]
   exact Iff.rfl
 
+/-- The slice of an intersection is the conjunction of the slices. -/
 @[simp] theorem slice_inf : (L ⊓ M).slice n x = (L.slice n x && M.slice n x) := by
   rw [Bool.eq_iff_iff, Bool.and_eq_true, slice_eq_true_iff, slice_eq_true_iff, slice_eq_true_iff]
   exact Iff.rfl
diff --git a/Complexity/Computability/QueryComplexity/Restriction.lean b/Complexity/Computability/QueryComplexity/Restriction.lean
index 85db06a3c..11313afc6 100644
--- a/Complexity/Computability/QueryComplexity/Restriction.lean
+++ b/Complexity/Computability/QueryComplexity/Restriction.lean
@@ -22,6 +22,11 @@ definitionally, so the generic restriction operations apply without conversions.
 * `Cslib.QueryComplexity.fill_restrict`: filling a coordinate certificate is a piecewise input.
 * `Cslib.QueryComplexity.forces_iff_forall_fill`: a forcing assignment makes the restricted
   function constant.
+
+## References
+
+* [H. Buhrman, R. de Wolf, *Complexity measures and decision tree complexity:
+  a survey*][BuhrmanDeWolf2002]
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Encoding.lean b/Complexity/Computability/TreeEval/Encoding.lean
index 0adaa26b6..4f879f6a6 100644
--- a/Complexity/Computability/TreeEval/Encoding.lean
+++ b/Complexity/Computability/TreeEval/Encoding.lean
@@ -36,6 +36,11 @@ offset `pathOffset`, which a machine can recompute from the path alone.
 * `Cslib.TreeEval.Tree.getElem_body_pathOffset`: the bits of the node at a path, read off the body
   at its offset; `Cslib.TreeEval.Tree.getElem_body_gate` and `Cslib.TreeEval.Tree.getElem_body_leaf`
   for gates and leaves.
+
+## References
+
+* [S. Cook, P. McKenzie, D. Wehr, M. Braverman and R. Santhanam, *Pebbles and branching programs
+  for tree evaluation*][CMWBS2012] introduce the problem, with gates given by their tables.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Reader/Arith.lean b/Complexity/Computability/TreeEval/Reader/Arith.lean
index 2a3fb1a73..c596cc8ed 100644
--- a/Complexity/Computability/TreeEval/Reader/Arith.lean
+++ b/Complexity/Computability/TreeEval/Reader/Arith.lean
@@ -31,6 +31,12 @@ the multilinear extension of a gate.
   bits of the inputs.
 * `Cslib.TreeEval.Reader.eval_gatePoly_eq_sum`: the multilinear extension of an output bit of a
   gate as a sum over the table indices `k < 4^ℓ`.
+
+## References
+
+* [J. Cook and I. Mertz, *Tree Evaluation is in Space O(log n · log log n)*][CookMertz2024]
+* [O. Goldreich, *On the Cook–Mertz Tree Evaluation procedure*][Goldreich2024TreeEval],
+  Algorithm 1, which the machine runs.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean b/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean
index b2e7eeefe..233d1b681 100644
--- a/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean
+++ b/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean
@@ -24,6 +24,12 @@ simulating it is tidy.
 ## Main results
 
 * `Cslib.TreeEval.Reader.tidy_machine`: the step machine simulating the read machine is tidy.
+
+## References
+
+* [J. Cook and I. Mertz, *Tree Evaluation is in Space O(log n · log log n)*][CookMertz2024]
+* [O. Goldreich, *On the Cook–Mertz Tree Evaluation procedure*][Goldreich2024TreeEval],
+  Algorithm 1, which the machine runs.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean b/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean
index 812844c6c..c33cdbd3f 100644
--- a/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean
+++ b/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean
@@ -44,6 +44,8 @@ theorem bodyLength_add_tableLength_le (ℓ d : ℕ) :
 def pathStep (ℓ : ℕ) (s : ℕ × ℕ) (b : Bool) : ℕ × ℕ :=
   if s.1 = 0 then s else (s.1 - 1, s.2 + tableLength ℓ + if b then bodyLength ℓ (s.1 - 1) else 0)
 
+/-- **The offset as a fold over the path**: folding `pathStep ℓ` over `P` from the height `d` and
+the sum `acc` gives the height `d - P.length` and the sum `acc + pathOffset ℓ d P`. -/
 theorem foldl_pathStep (ℓ : ℕ) (P : List Bool) :
     ∀ d acc, P.foldl (pathStep ℓ) (d, acc) = (d - P.length, acc + pathOffset ℓ d P) := by
   induction P with
diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Step.lean b/Complexity/Computability/TreeEval/Reader/Cert/Step.lean
index 4bea27e1d..20552714f 100644
--- a/Complexity/Computability/TreeEval/Reader/Cert/Step.lean
+++ b/Complexity/Computability/TreeEval/Reader/Cert/Step.lean
@@ -28,6 +28,12 @@ prime and the round of the top frame together. On the states the machine reaches
 ## Main results
 
 * `Cslib.TreeEval.Reader.stepT_inSpace`: the step within the budget.
+
+## References
+
+* [J. Cook and I. Mertz, *Tree Evaluation is in Space O(log n · log log n)*][CookMertz2024]
+* [O. Goldreich, *On the Cook–Mertz Tree Evaluation procedure*][Goldreich2024TreeEval],
+  Algorithm 1, which the machine runs.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Reader/Defs.lean b/Complexity/Computability/TreeEval/Reader/Defs.lean
index a11179f3e..a002690cd 100644
--- a/Complexity/Computability/TreeEval/Reader/Defs.lean
+++ b/Complexity/Computability/TreeEval/Reader/Defs.lean
@@ -30,6 +30,12 @@ register `2`.
 
 * `Cslib.TreeEval.Reader.State`: the states of the machine.
 * `Cslib.TreeEval.Reader.machine`: the machine.
+
+## References
+
+* [J. Cook and I. Mertz, *Tree Evaluation is in Space O(log n · log log n)*][CookMertz2024]
+* [O. Goldreich, *On the Cook–Mertz Tree Evaluation procedure*][Goldreich2024TreeEval],
+  Algorithm 1, which the machine runs.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Reader/Size.lean b/Complexity/Computability/TreeEval/Reader/Size.lean
index 05540e519..d9909898c 100644
--- a/Complexity/Computability/TreeEval/Reader/Size.lean
+++ b/Complexity/Computability/TreeEval/Reader/Size.lean
@@ -27,6 +27,12 @@ of them, the stack holds at most `H` frames with a residue each, and the counter
 ## Main results
 
 * `Cslib.TreeEval.Reader.stateBudget_le`: the budget of every state reached is `O(spaceBound ℓ H)`.
+
+## References
+
+* [J. Cook and I. Mertz, *Tree Evaluation is in Space O(log n · log log n)*][CookMertz2024]
+* [O. Goldreich, *On the Cook–Mertz Tree Evaluation procedure*][Goldreich2024TreeEval],
+  Algorithm 1, which the machine runs.
 -/
 
 @[expose] public section
diff --git a/Complexity/Computability/TreeEval/Reader/Tuple.lean b/Complexity/Computability/TreeEval/Reader/Tuple.lean
index 72a53ac78..ef0044a16 100644
--- a/Complexity/Computability/TreeEval/Reader/Tuple.lean
+++ b/Complexity/Computability/TreeEval/Reader/Tuple.lean
@@ -167,14 +167,18 @@ def stepT (y : Tuple × Bool) : Tuple × List Bool :=
       ({ fr with phase := 2 } :: x.stack.tail) (.call true (fr.target + 1)) runCtl, [])
   else (x, [])
 
+/-- On the tuple of a state, `haltT` is the halting test of `machine`. -/
 theorem haltT_toTuple (s : State) : haltT s.toTuple = machine.halt s := by
   obtain ⟨_, _, _, _, _, _, c⟩ := s
   cases c <;> rfl
 
+/-- On the tuple of a state, `addrT` is the address `addr` of the state. -/
 theorem addrT_toTuple (s : State) : addrT s.toTuple = addr s := by
   obtain ⟨_, _, _, _, _, _, c⟩ := s
   cases c <;> rfl
 
+/-- On the tuple of a state, `stepT` is the step of `machine`: it gives the tuple of the next
+state and the same output. -/
 theorem stepT_toTuple (s : State) (b : Bool) :
     stepT (s.toTuple, b) = ((machine.step s b).1.toTuple, (machine.step s b).2) := by
   obtain ⟨e, h, p, R, st, m, c⟩ := s
diff --git a/Complexity/Computability/USTCON/Reader/Cert.lean b/Complexity/Computability/USTCON/Reader/Cert.lean
index 1e2f579de..11cbd8c6f 100644
--- a/Complexity/Computability/USTCON/Reader/Cert.lean
+++ b/Complexity/Computability/USTCON/Reader/Cert.lean
@@ -471,13 +471,17 @@ noncomputable def stateBudget (q : State) : ℕ :=
 theorem stepBudget_bool (x : Tuple) (b : Bool) : stepBudget (x, b) = stepBudget (x, false) := by
   cases b <;> simp [stepBudget, encBool_apply]
 
+/-- The halting test of `machine` is tidily computable within the space budget of the state. -/
 theorem halt_inSpace : ComputableTidilyInSpace machine.halt encState encBool stateBudget :=
   (haltT_inSpace.of_encIn_eq State.toTuple fun _ ↦ rfl).of_enc_eq fun _ ↦ rfl
 
+/-- The address of `machine` is tidily computable within the space budget of the state. -/
 theorem addr_inSpace : ComputableTidilyInSpace machine.addr encState (encOption encNat)
     stateBudget :=
   (addrT_inSpace.of_encIn_eq State.toTuple fun _ ↦ rfl).of_enc_eq fun _ ↦ rfl
 
+/-- The step of `machine`, on a state and the bit read, is tidily computable within the space
+budget of the state. -/
 theorem step_inSpace :
     ComputableTidilyInSpace (fun p : State × Bool => machine.step p.1 p.2)
       (encPair encState encBool) (encPair encState encBits) fun p => stateBudget p.1 := by