diff --git a/Complexity.lean b/Complexity.lean
index e61298bb50..37103319bb 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -834,6 +834,7 @@ public import Complexity.Computability.GenericRAM.Simulation.Turing
 public import Complexity.Computability.GenericRAM.SparseMemory.Basic
 public import Complexity.Computability.GenericRAM.SparseMemory.Turing
 public import Complexity.Computability.Interactive.Basic
+public import Complexity.Computability.Interactive.GKR.Layered
 public import Complexity.Computability.Interactive.Plain
 public import Complexity.Computability.Interactive.Security
 public import Complexity.Computability.Interactive.Sequential
diff --git a/Complexity/Computability/Interactive/GKR/Layered.lean b/Complexity/Computability/Interactive/GKR/Layered.lean
new file mode 100644
index 0000000000..b8ed089100
--- /dev/null
+++ b/Complexity/Computability/Interactive/GKR/Layered.lean
@@ -0,0 +1,192 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.BooleanAnalysis.MultilinearExtension
+
+/-!
+# Layered arithmetic circuits and the GKR identity
+
+A *layered arithmetic circuit* of fan-in two (`Cslib.Interactive.GKR.LayeredCircuit`) has its gates
+arranged in layers, with the gates of layer `i` labelled by the bit strings of length `width i`.
+Layer `0` is the input. Every gate of layer `i + 1` is an addition or a multiplication of two gates
+of layer `i`, its left and right in-neighbours. Evaluating the layers in turn gives the gate values
+`value x i` on an input `x` (`Cslib.Interactive.GKR.LayeredCircuit.value`). We number the layers
+from the input, while [Thaler, §4.6][Thaler2022] numbers them from the output.
+
+The *wiring predicates* `add_i (a, b, c)` and `mult_i (a, b, c)` of layer `i + 1` are `1` exactly
+when gate `a` of layer `i + 1` is an addition, respectively a multiplication, with in-neighbours
+`b` and `c` (`addPred`, `multPred`). The identity at the heart of the GKR protocol expresses the
+multilinear extension of the gate values of a layer through the multilinear extensions of the
+wiring predicates and the gate values of the layer below
+(`Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_step`)
+[Thaler, Lemma 4.7][Thaler2022], [Goldwasser, Kalai, Rothblum][GoldwasserKalaiRothblum2015]:
+`W̃_{i+1}(z) = ∑_{b, c} ãdd_i(z, b, c) (W_i(b) + W_i(c)) + m̃ult_i(z, b, c) W_i(b) W_i(c)`.
+
+## Main definitions
+
+* `Cslib.Interactive.GKR.LayeredCircuit`: a layered arithmetic circuit of fan-in two.
+* `Cslib.Interactive.GKR.LayeredCircuit.step`, `Cslib.Interactive.GKR.LayeredCircuit.value`:
+  evaluation of one layer and of the circuit.
+* `Cslib.Interactive.GKR.LayeredCircuit.addPred`, `Cslib.Interactive.GKR.LayeredCircuit.multPred`:
+  the wiring predicates.
+
+## Main results
+
+* `Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_wiringPred`: the closed form of
+  the multilinear extensions of the wiring predicates (`addPred` and `multPred` are its two cases).
+* `Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_step`: the GKR identity.
+
+## References
+
+* [S. Goldwasser, Y. T. Kalai, G. N. Rothblum, *Delegating computation: interactive proofs for
+  muggles*][GoldwasserKalaiRothblum2015]
+* [J. Thaler, *Proofs, Arguments, and Zero-Knowledge*][Thaler2022], Section 4.6
+-/
+
+@[expose] public section
+
+namespace Cslib.Interactive.GKR
+
+open MvPolynomial Cslib.BitString
+
+/-- The two kinds of gates of an arithmetic circuit of fan-in two. -/
+inductive Gate
+  /-- An addition gate. -/
+  | add
+  /-- A multiplication gate. -/
+  | mul
+  deriving DecidableEq
+
+/-- A **layered arithmetic circuit** of fan-in two. The gates of layer `i` are labelled by bit
+strings of length `width i`; layer `0` is the input, and each gate of layer `i + 1` combines two
+gates of layer `i`. -/
+structure LayeredCircuit where
+  /-- The number of layers above the input. -/
+  depth : ℕ
+  /-- Layer `i` has `2 ^ width i` gates. -/
+  width : ℕ → ℕ
+  /-- The kind of each gate of layer `i + 1`. -/
+  gate : (i : ℕ) → (Fin (width (i + 1)) → Bool) → Gate
+  /-- The left in-neighbour, in layer `i`, of each gate of layer `i + 1`. -/
+  left : (i : ℕ) → (Fin (width (i + 1)) → Bool) → Fin (width i) → Bool
+  /-- The right in-neighbour, in layer `i`, of each gate of layer `i + 1`. -/
+  right : (i : ℕ) → (Fin (width (i + 1)) → Bool) → Fin (width i) → Bool
+
+namespace LayeredCircuit
+
+variable (C : LayeredCircuit) {R : Type*} [CommRing R]
+
+/-- The values of layer `i + 1`, given the values `W` of layer `i`. -/
+def step (i : ℕ) (W : (Fin (C.width i) → Bool) → R) (a : Fin (C.width (i + 1)) → Bool) : R :=
+  match C.gate i a with
+  | .add => W (C.left i a) + W (C.right i a)
+  | .mul => W (C.left i a) * W (C.right i a)
+
+/-- The gate values of layer `i` on the input `x`. -/
+def value (x : (Fin (C.width 0) → Bool) → R) : (i : ℕ) → (Fin (C.width i) → Bool) → R
+  | 0 => x
+  | i + 1 => C.step i (value x i)
+
+/-- The output values of the circuit. -/
+def output (x : (Fin (C.width 0) → Bool) → R) : (Fin (C.width C.depth) → Bool) → R :=
+  C.value x C.depth
+
+/-- The variables of a wiring predicate of layer `i + 1`: a gate `a` of layer `i + 1` and two gates
+`b`, `c` of layer `i`. -/
+abbrev WiringVar (i : ℕ) : Type := Fin (C.width (i + 1)) ⊕ (Fin (C.width i) ⊕ Fin (C.width i))
+
+/-- The wiring predicate of a gate kind: `1` exactly when gate `a` of layer `i + 1` has that kind
+and in-neighbours `b` and `c`. -/
+def wiringPred (g : Gate) (i : ℕ) (v : C.WiringVar i → Bool) : R :=
+  open Classical in
+  if C.gate i (v ∘ Sum.inl) = g ∧ C.left i (v ∘ Sum.inl) = v ∘ Sum.inr ∘ Sum.inl ∧
+      C.right i (v ∘ Sum.inl) = v ∘ Sum.inr ∘ Sum.inr then 1 else 0
+
+/-- The addition predicate `add_i`. -/
+abbrev addPred (i : ℕ) : (C.WiringVar i → Bool) → R := C.wiringPred .add i
+
+/-- The multiplication predicate `mult_i`. -/
+abbrev multPred (i : ℕ) : (C.WiringVar i → Bool) → R := C.wiringPred .mul i
+
+/-- The multilinear extension of a wiring predicate at `(z, y, w)` is the sum, over the gates `a`
+of that kind, of the product of the basis polynomials of `a`, its left and its right in-neighbour.
+-/
+theorem eval_multilinearExtension_wiringPred (g : Gate) (i : ℕ) (z : Fin (C.width (i + 1)) → R)
+    (y w : Fin (C.width i) → R) :
+    eval (Sum.elim z (Sum.elim y w)) (multilinearExtension (C.wiringPred (R := R) g i)) =
+      ∑ a, if C.gate i a = g then eval z (indicatorPoly a) * eval y (indicatorPoly (C.left i a)) *
+          eval w (indicatorPoly (C.right i a))
+        else 0 := by
+  simp only [multilinearExtension, map_sum, map_mul, eval_C, eval_indicatorPoly_apply]
+  rw [← (Equiv.sumArrowEquivProdArrow _ _ Bool).symm.sum_comp, Fintype.sum_prod_type]
+  refine Finset.sum_congr rfl fun a _ => ?_
+  rw [← (Equiv.sumArrowEquivProdArrow _ _ Bool).symm.sum_comp, Fintype.sum_prod_type]
+  simp only [Equiv.sumArrowEquivProdArrow_symm_apply_inl, Fintype.prod_sum_type,
+    Sum.elim_inl, Sum.elim_inr, wiringPred]
+  by_cases hg : C.gate i a = g
+  · rw [ite_eq_left hg]
+    rw [Finset.sum_eq_single (C.left i a), Finset.sum_eq_single (C.right i a)]
+    · simp only [Function.comp_def, Equiv.sumArrowEquivProdArrow_symm_apply_inl, hg,
+        Equiv.sumArrowEquivProdArrow_symm_apply_inr, and_self, ↓reduceIte, one_mul, mul_assoc]
+      congr 1
+    · intro c _ hc
+      simp [Function.comp_def, Ne.symm hc]
+    · simp
+    · intro b _ hb
+      refine Finset.sum_eq_zero fun c _ => ?_
+      simp [Function.comp_def, Ne.symm hb]
+    · simp
+  · rw [ite_eq_right hg]
+    refine Finset.sum_eq_zero fun b _ => Finset.sum_eq_zero fun c _ => ?_
+    simp [Function.comp_def, hg]
+
+/-- **The GKR identity** [Thaler, Lemma 4.7][Thaler2022]. The multilinear extension of the values
+of layer `i + 1` is a sum over the pairs of gates `b`, `c` of layer `i` of the multilinear
+extensions of the wiring predicates times the sum, respectively the product, of the values of `b`
+and `c`. -/
+theorem eval_multilinearExtension_step (i : ℕ) (W : (Fin (C.width i) → Bool) → R)
+    (z : Fin (C.width (i + 1)) → R) :
+    eval z (multilinearExtension (C.step i W)) =
+      ∑ b, ∑ c,
+        (eval (Sum.elim z (Sum.elim (bitPoint b) (bitPoint c)))
+            (multilinearExtension (C.addPred (R := R) i)) * (W b + W c) +
+          eval (Sum.elim z (Sum.elim (bitPoint b) (bitPoint c)))
+            (multilinearExtension (C.multPred (R := R) i)) * (W b * W c)) := by
+  rw [eval_multilinearExtension_eq_sum (C.step i W)]
+  simp only [eval_multilinearExtension_wiringPred, eval_indicatorPoly]
+  have hinner : ∀ b c, (∑ a, if C.gate i a = .add then eval z (indicatorPoly a) *
+        (if C.left i a = b then (1 : R) else 0) * (if C.right i a = c then 1 else 0) else 0) *
+        (W b + W c) +
+      (∑ a, if C.gate i a = .mul then eval z (indicatorPoly a) *
+        (if C.left i a = b then (1 : R) else 0) * (if C.right i a = c then 1 else 0) else 0) *
+        (W b * W c) =
+      ∑ a, (if C.left i a = b ∧ C.right i a = c then eval z (indicatorPoly a) *
+        (if C.gate i a = .add then W b + W c else W b * W c) else 0) := by
+    intro b c
+    rw [Finset.sum_mul, Finset.sum_mul, ← Finset.sum_add_distrib]
+    refine Finset.sum_congr rfl fun a _ => ?_
+    by_cases hb : C.left i a = b <;> by_cases hc : C.right i a = c <;>
+      cases C.gate i a <;> simp [hb, hc]
+  simp only [hinner]
+  symm
+  refine (Finset.sum_congr rfl fun b _ => Finset.sum_comm).trans (Finset.sum_comm.trans ?_)
+  refine Finset.sum_congr rfl fun a _ => ?_
+  rw [Finset.sum_eq_single (C.left i a), Finset.sum_eq_single (C.right i a)]
+  · simp only [and_self, ite_true, step]
+    cases C.gate i a <;> simp [mul_comm]
+  · intro c _ hc
+    simp [Ne.symm hc]
+  · simp
+  · intro b _ hb
+    exact Finset.sum_eq_zero fun c _ => by simp [Ne.symm hb]
+  · simp
+
+end LayeredCircuit
+
+end Cslib.Interactive.GKR
diff --git a/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean b/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean
index 5de569b8aa..56b616698d 100644
--- a/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean
+++ b/Complexity/Foundations/BooleanAnalysis/MultilinearExtension.lean
@@ -28,6 +28,8 @@ Its total degree is at most the dimension.
 ## Main results
 
 * `Cslib.BitString.eval_multilinearExtension`: the extension agrees with the function on the cube.
+* `Cslib.BitString.eval_multilinearExtension_eq_sum`: the extension at any point, in the indicator
+  basis.
 * `Cslib.BitString.totalDegree_multilinearExtension_le`: its total degree is at most the
   dimension.
 * `Cslib.BitString.rename_multilinearExtension`: renaming the coordinates along an equivalence
@@ -74,6 +76,15 @@ theorem eval_indicatorPoly [Fintype ι] (a x : ι → Bool) :
     exact Finset.prod_eq_zero (Finset.mem_univ i)
       (by cases ha : a i <;> cases hx : x i <;> simp_all)
 
+/-- The point of `R^ι` with the coordinates of the bit string `x`. -/
+abbrev bitPoint (x : ι → Bool) : ι → R := fun i => bitVal R (x i)
+
+/-- The multilinear extension at any point is the sum of the values of the function weighted by the
+indicator polynomials. -/
+theorem eval_multilinearExtension_eq_sum [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → R)
+    (z : ι → R) : eval z (multilinearExtension g) = ∑ a, g a * eval z (indicatorPoly a) := by
+  simp [multilinearExtension]
+
 /-- The multilinear extension agrees with the function on the cube. -/
 theorem eval_multilinearExtension [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → R)
     (x : ι → Bool) : eval (fun i => bitVal R (x i)) (multilinearExtension g) = g x := by
diff --git a/ComplexityTests/GKRLayered.lean b/ComplexityTests/GKRLayered.lean
new file mode 100644
index 0000000000..b166534c0a
--- /dev/null
+++ b/ComplexityTests/GKRLayered.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Interactive.GKR.Layered
+
+/-! # Layered arithmetic circuits and the GKR identity
+
+A one-layer circuit multiplying its two inputs, its value, and an instance of the GKR identity.
+-/
+
+namespace ComplexityTests.GKRLayered
+
+open Cslib.Interactive.GKR MvPolynomial Cslib.BitString
+
+/-- One multiplication gate on two inputs: layer `0` has `2 ^ 1` gates, layer `1` has `2 ^ 0`. -/
+def mulTwo : LayeredCircuit where
+  depth := 1
+  width := fun i => if i = 0 then 1 else 0
+  gate _ _ := .mul
+  left _ _ := fun _ => false
+  right _ _ := fun _ => true
+
+-- The output is the product of the two inputs.
+example (x : (Fin 1 → Bool) → ℤ) :
+    mulTwo.output x (fun _ => false) = x (fun _ => false) * x (fun _ => true) := rfl
+
+-- The GKR identity for the multiplication layer, at any point.
+example (W : (Fin (mulTwo.width 0) → Bool) → ℤ) (z : Fin (mulTwo.width 1) → ℤ) :
+    eval z (multilinearExtension (mulTwo.step 0 W)) =
+      ∑ b, ∑ c,
+        (eval (Sum.elim z (Sum.elim (bitPoint b) (bitPoint c)))
+            (multilinearExtension (mulTwo.addPred (R := ℤ) 0)) * (W b + W c) +
+          eval (Sum.elim z (Sum.elim (bitPoint b) (bitPoint c)))
+            (multilinearExtension (mulTwo.multPred (R := ℤ) 0)) * (W b * W c)) :=
+  mulTwo.eval_multilinearExtension_step 0 W z
+
+/--
+info: 'Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_step' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms LayeredCircuit.eval_multilinearExtension_step
+
+/--
+info: 'Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_wiringPred' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms LayeredCircuit.eval_multilinearExtension_wiringPred
+
+end ComplexityTests.GKRLayered
diff --git a/ROADMAP.md b/ROADMAP.md
index 892f65548f..c1883e20a1 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -1266,6 +1266,11 @@ Jukna coverage below is an additional target beyond the V1 port:
     components, stated as theory without concrete ciphersuites.
 
   The design is on #643, and the TQBF, PCP and GMW bridges are recorded there.
+* **GKR delegation (#892).** [Layered](Complexity/Computability/Interactive/GKR/Layered.lean)
+  defines layered arithmetic circuits and proves the GKR identity expressing the multilinear
+  extension of a layer through the wiring predicates and the layer below. Open: the GKR protocol
+  itself (layer-by-layer sumcheck and the line reduction, with completeness and soundness), its
+  efficiency under uniformity, and the route to NEXP ⊆ MIP.
 * **Classic symmetric constructions (#640, track D).** Proved: PRF-based MACs (#677), keyed
   collision-resistant hash families and Merkle–Damgård (#678), universal hashing (#663),
   [Carter–Wegman MACs from Δ-universal hashing](Complexity/Crypto/Protocols/MAC/CarterWegman.lean)
diff --git a/references.bib b/references.bib
index 987485363f..38e90da6b7 100644
--- a/references.bib
+++ b/references.bib
@@ -1667,6 +1667,17 @@ @article{Goldschlager1977
   doi       = {10.1145/1008354.1008356}
 }
 
+@article{GoldwasserKalaiRothblum2015,
+  author  = {Goldwasser, Shafi and Kalai, Yael Tauman and Rothblum, Guy N.},
+  title   = {Delegating Computation: Interactive Proofs for Muggles},
+  journal = {Journal of the ACM},
+  volume  = {62},
+  number  = {4},
+  pages   = {27:1--27:64},
+  year    = {2015},
+  doi     = {10.1145/2699436}
+}
+
 @article{GoldwasserMicaliRackoff1989,
   author  = {Goldwasser, Shafi and Micali, Silvio and Rackoff, Charles},
   title   = {The Knowledge Complexity of Interactive Proof Systems},
@@ -3711,6 +3722,17 @@ @article{Tardos1989
   year      = {1989}
 }
 
+@article{Thaler2022,
+  author  = {Thaler, Justin},
+  title   = {Proofs, Arguments, and Zero-Knowledge},
+  journal = {Foundations and Trends in Privacy and Security},
+  volume  = {4},
+  number  = {2--4},
+  pages   = {117--660},
+  year    = {2022},
+  doi     = {10.1561/3300000030}
+}
+
 @incollection{ Thomas1990,
   author       = {Wolfgang Thomas},
   editor       = {Jan van Leeuwen},