ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A two-quantifier field transcript

Example

Work over the prime field $F = Z / 251$ , and take the closed prenex quantified Boolean formula $Φ = \exists x \forall y (x \lor \neg y),$ whose matrix is $ψ = x \lor \neg y$ and which is true, since $x = 1$ makes the matrix $1$ for both values of $y$ . The matrix has $L = 4$ syntax nodes, so with $n = 2$ the protocol has $D = 4$ , $T = 5$ , and $N = 241$ ; $p = 251$ is the first prime greater than $N$ . Its matrix arithmetization is $b (X, Y) = 1 - Y + X Y,$ the multilinearized operator sequence of $Φ$ is $b \overset{R_{X}}{\to} R_{X} b \overset{R_{Y}}{\to} R_{Y} R_{X} b \overset{A_{Y}}{\to} A_{Y} R_{Y} R_{X} b \overset{R_{X}}{\to} R_{X} A_{Y} R_{Y} R_{X} b \overset{E_{X}}{\to} 1,$ and the reverse protocol of The Shamir interactive protocol for TQBF processes the nodes $E_{X}$ , then $R_{X}$ , then $A_{Y}$ , $R_{Y}$ , $R_{X}$ , with challenges drawn in the order $2, 3, 4, 5, 6$ . With those challenges the honest claim sequence is $1 \to 2 \to 3 \to 9 \to 11 \to 26$ and the terminal comparison is $b (6, 5) = 26$ .

Facts & Assumptions

Given: The field $Z / 251$ , the formula $Φ = \exists x \forall y (x \lor \neg y)$ and the protocol of The Shamir interactive protocol for TQBF for it.

[A1]

Arithmetization replaces $\neg u$ and $u \lor v$ by $1 - u$ and $u + v - u v$ , variable leaves by their variables, and it agrees with the Boolean value of the formula at Boolean inputs (Arithmetization of Boolean formulas).

[A2]

The ordered arithmetization applies $A_{X} P = (P ∣_{X = 0}) (P ∣_{X = 1})$ and $E_{X} P = 1 - (1 - P ∣_{X = 0}) (1 - P ∣_{X = 1})$ to the quantifiers, inner quantifiers first (Field arithmetization of QBF quantifiers).

[A3]

The multilinearized sequence inserts $R_{X} P = (1 - X) (P ∣_{X = 0}) + X (P ∣_{X = 1})$ before each quantifier operation, and its blocks for the prefix $\exists x \forall y$ are $R_{X}, R_{Y}, A_{Y}$ followed by $R_{X}, E_{X}$ (Multilinearization in one variable).

[A4]

In the protocol the rounds process the operator list backwards; in the round for a node the verifier tests $c = s (0) s (1)$ for $A$ , $c = s (0) + s (1) - s (0) s (1)$ for $E$ , and $c = (1 - a) s (0) + a s (1)$ with the current value $a$ of the reduced variable for $R$ , then samples a fresh challenge $r$ , sets the reduced variable to $r$ and $c : = s (r)$ , and finally accepts exactly when $c = b (σ)$ (The Shamir interactive protocol for TQBF).

[A5]

The classes of $Z / 251$ form a field under addition and multiplication modulo $251$ (For every prime $p$ , the two operations on $Z / p$ make it a field), and $Φ$ is a closed prenex quantified Boolean formula with the truth semantics of Quantified Boolean formulas and the language TQBF.

Verification

1.1

By [A1] the matrix arithmetization is $X + (1 - Y) - X (1 - Y)$ , which simplifies to $1 - Y + X Y = : b (X, Y)$ . At the four Boolean points it takes the values $b (0, 0) = 1$ , $b (0, 1) = 0$ , $b (1, 0) = 1$ , $b (1, 1) = 1$ , matching $x \lor \neg y$ in each case.

A1algebra

2.1

The reductions do not change $b$ , because $b$ is multilinear: $b ∣_{X = 0} = 1 - Y$ and $b ∣_{X = 1} = 1$ give $R_{X} b = (1 - X) (1 - Y) + X = 1 - Y + X Y$ , and $b ∣_{Y = 0} = 1$ and $b ∣_{Y = 1} = X$ give $R_{Y} b = (1 - Y) + Y X = 1 - Y + X Y$ .

A3step 1.1algebra

3.1

Applying the quantifier operations: $A_{Y} b = (b ∣_{Y = 0}) (b ∣_{Y = 1}) = 1 \cdot X = X$ , then $R_{X} X = X$ since $X ∣_{X = 0} = 0$ and $X ∣_{X = 1} = 1$ , and finally $E_{X} X = 1 - (1 - 0) \cdot (1 - 1) = 1$ . The constant so obtained is the truth value of $Φ$ by [A2] and [A5], and indeed $Φ$ is true.

A2step 2.1A5algebra

3.2

Reading the stages backwards, the honest messages are the restrictions of $G_{4} = R_{X} X = X$ , $G_{3} = X$ , $G_{2} = R_{Y} R_{X} b = 1 - Y + X Y$ at $x = 3$ , $G_{1} = 1 - Y + X Y$ at $x = 3$ , and $G_{0} = b$ at $y = 5$ ; that is, in the order of the rounds, $s_{1} (T) = T$ , $s_{2} (T) = T$ , $s_{3} (T) = 1 + 2 T$ , $s_{4} (T) = 1 + 2 T$ and $s_{5} (T) = 5 T - 4$ .

A3A4step 2.1algebra

4.1

The reverse protocol of [A4] therefore processes $E_{X}$ first, then $R_{X}$ , then $A_{Y}$ , $R_{Y}$ and $R_{X}$ . Take the challenges in this order to be $2, 3, 4, 5, 6$ , so that $σ (x)$ is set to $2$ and then to $3$ and finally to $6$ , and $σ (y)$ is set to $4$ and then to $5$ .

A4step 3.1

4.2

The verifier's tests pass with these messages: $E_{X}$ checks $1 = 0 + 1 - 0$ ; then $R_{X}$ with $a = 2$ checks $2 = (1 - 2) \cdot 0 + 2 \cdot 1$ ; then $A_{Y}$ checks $3 = 1 \cdot 3$ , where $s_{3} (0) = 1$ and $s_{3} (1) = 3$ ; then $R_{Y}$ with $a = 4$ checks $9 = (1 - 4) \cdot 1 + 4 \cdot 3$ ; and finally $R_{X}$ with $a = 3$ checks $11 = (1 - 3) \cdot (- 4) + 3 \cdot 1$ . So the claim sequence is $1 \to 2 \to 3 \to 9 \to 11 \to 26$ , where each new claim is obtained by evaluating the sent message at the new challenge.

A4step 3.2algebra

5.1

The point left at the end is $σ = (6, 5)$ , and the terminal comparison gives $b (6, 5) = 1 - 5 + 30 = 26$ , equal to the final claim $26$ ; the verifier therefore accepts this transcript. All products and sums above are computed in $Z / 251$ , where $(1 - 4) \cdot 1 = - 3 \equiv 248$ and $248 + 12 = 260 \equiv 9 (m o d 251)$ , so the intermediate values agree with the field arithmetic.

A4step 4.2A5algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. Shen, IP = PSPACE: Simplified Proof, JACM 39(4) 1992, pp. 878–880 (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §8.5.3, author-hosted draft (standard reference, not scraped)