A proof complexity perspective on effectively zero-knowledge proofs

Jan Krajicek

REVIEW 3 major objections 4 minor 16 references

A proof complexity perspective on effectively zero-knowledge proofs

T0 review · 3 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Hard tautologies make zero-knowledge a provability phenomenon: a NIWI-based prover for SAT is zero-knowledge relative to a theory when the statement 'no small simulator exists' has no short proof in that theory, and a shared random string t

desk verdict The Sec. 2 logical reformulation of effectively ZK is a real contribution, but the Sec. 3 claim to genuine ZK does not survive contact with the standard model. read the letter →

arxiv 2607.13540 v1 pith:CFFQI4MN submitted 2026-07-15 cs.CC math.LO

Jan Krajicek This is my paper · ORCID

classification cs.CCmath.LO MSC 03F2068Q15

keywords proofcomplexityzero-knowledgeproofseffectivelynon-interactivewitnessindistinguishabilityboundedarithmeticgeneratorspropositionaltautologiescommonrandomstring

topics P versus NP

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that zero-knowledge can be redefined in proof-theoretic terms, replacing the usual requirement that a simulator exists with the requirement that the absence of a simulator is hard to prove. Under a hardness assumption about propositional tautologies, it shows that a simple non-interactive witness-indistinguishable prover for SAT is zero-knowledge in this logical sense. The reformulation derives the 'indistinguishable from true' property as a consequence rather than building it into the definition. It then shows that, with a shared random string and a hard proof-complexity generator, this logical zero-knowledge can be upgraded to zero-knowledge in the usual cryptographic sense.

What carries the argument

The key mechanism is the model-theoretic equivalence from bounded arithmetic: a propositional formula is not provable in the proof system P(T) exactly when there is an extension of a model of T in which the formula is falsified. This lets the proof translate 'Ψ is hard for P(T*)' into 'there is a non-standard model containing a simulator circuit', which is what makes the zero-knowledge claim go through. The second mechanism is the τ-formula of a proof-complexity generator: τ(g_s)^b is a tautology exactly when b lies outside the range of g_s. A generator hard for all propositional proof systems therefore supplies a p-time sequence of hard tautologies, which the shared-random-string constructi

What would settle it

Find a propositional proof system that proves every p-time tautology sequence in size polynomial in the formula length; then no sequence Ψ can be hard for that system, so the hypothesis of Theorem 2.2 fails. For the generator upgrade, exhibit a specific proof system that, for every seed s and every b, proves τ(g_s)^b in polynomial size; that would refute the hard-generator claim on which the ordinary zero-knowledge construction rests.

Watch

Extended reading notes

Core claim

The central claim is that, under the assumptions that the base theory T is true and contains enough arithmetic, that (A,B) is a NIWI pair, and that a p-time sequence of tautologies Ψ is hard for the proof system P(T*), the prover Prover[A,B,Ψ] is ZK relative to T. Concretely, for every c,e ≥ 1 and all sufficiently large n, there is no T-proof of size at most n^e of the sentence asserting that no circuit of size at most n^d is a simulator for the prover. The proof uses a model-theoretic equivalence: if Ψ is not provable in P(T*), then a non-standard model can be extended to one where Ψ is false, and in that extension a simulator circuit can be built. The paper also proves that this definition

Load-bearing premise

The argument stands or falls with the assumption that there exists a p-time sequence of tautologies that is hard for the proof system P(T*); this is equivalent to there being no propositional proof system that has only polynomial slowdown over all others.

Editorial extensions

If this is right

Provided the hardness assumption holds, SAT admits a non-interactive zero-knowledge proof in the logical sense, with no interaction and no setup beyond the NIWI.
The 'indistinguishable from true' property follows automatically from the definition, so it does not need to be imposed as a separate condition.
With a shared random string and a hard proof-complexity generator, the logical zero-knowledge protocol becomes zero-knowledge in the ordinary cryptographic sense.
The verifier cannot prove the protocol sound from within the base theory, because soundness depends on tautologies whose tautologyhood the theory itself cannot establish.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: the logical definition suggests a hierarchy of zero-knowledge notions indexed by the strength of T; weaker theories make the absence of a simulator harder to prove, so protocols could remain zero-knowledge even as actual simulators start to appear.
Editorial inference: the soundness of the generator-based protocol is tied to the range-avoidance problem; any algorithm that finds b in the range of g_s would make τ(g_s)^b falsifiable and break both soundness and the zero-knowledge argument.
Editorial inference: if the hard-generator conjecture holds, the common random string could plausibly be an ordinary public random string, removing the need for a trusted setup in these protocols.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The core of this paper, Sec. 2, is worth reading. Krajicek recasts Ilango's effectively zero-knowledge proofs in bounded arithmetic, defines ZK relative to a theory, and proves existence under the same assumptions. The genuinely new and good part is that 'indistinguishable from true' falls out as a theorem (Thm 2.4) instead of being baked into the definition. The model-theoretic proof of Thm 2.2 via the K-P theorem and overspill is standard and, as far as I can check, sound. That is a clean conceptual improvement over Ilango, and it alone justifies a serious look.

The soft spots are concentrated in Sec. 3. The claim that replacing ψ_n with τ(g_s)^b and a shared random string yields ZK 'in the usual sense' is not supported. The stress-test note is right: the simulator in Thm 2.2 works by picking a nonstandard assignment v* that falsifies the tautology. When τ(g_s)^b is a genuine standard tautology (i.e., b is outside the range of g_s), no such v* exists in the standard universe. The dummy-witness trick used throughout the paper—witness (0,v) for φ∨¬τ—therefore has no standard realization, and no other standard simulator is supplied. The hardness Claim, even if proved, only says these tautologies are hard; it does not give a way to generate a fake witness in the standard world. So the construction, at best, preserves ZK relative to T, which is a strictly weaker notion.

Other issues are real but less severe: the hard-sequence assumption on Ψ is conjectural and the paper itself notes no construction is known; the Sec. 3 Claim comes from a companion paper without proof; and protocol soundness is unverifiable by the parties, a limitation the author concedes. These are more 'incomplete' than 'wrong'. But the Sec. 3 overclaim is a load-bearing flaw in the advertised contribution.

Who is this for? People working in proof complexity and the logical foundations of zero knowledge. The Sec. 2 material deserves peer review; Sec. 3 should either be proved or explicitly downgraded to a conjecture. I would send it to a referee, but with a clear request to fix or fence off Sec. 3.

Referee Report

3 major / 4 minor

Summary. The paper reformulates Ilango's effectively zero-knowledge proofs in the language of bounded arithmetic. Under the assumptions that T is a true p-time axiomatized theory containing S_2^1, that (A,B) is a NIWI, and that there is a p-time construable sequence of tautologies Ψ hard for P(T*), the author defines a p-time prover Prover[A,B,Ψ] and proves (Theorem 2.2) that it is ZK relative to T: for every c,e≥1, no T-proof of size ≤n^e can prove the nonexistence of a size ≤n^d simulator. The definition does not include the 'indistinguishable from true' property; instead Theorem 2.4 derives it as a consequence. Section 3 discusses the difficulty of constructing the required hard tautologies and then outlines an attempt, based on proof-complexity generators and a shared random string, to turn the construction into genuinely zero-knowledge proofs in the usual sense. The main advertised upgrade in Section 3 is, however, not established.

Significance. The Section 2 reformulation is a genuine contribution: it gives a short, modular proof using the Krajíček–Pudlák theorem and nonstandard models, and it shows that 'indistinguishable from true' can be a theorem rather than a definitional requirement. The paper is also honest about the conditional nature of the main existence result and about the lack of known constructions for the hard tautology sequence. If the Section 3 upgrade worked, it would be a notable connection between proof-complexity generators and zero-knowledge. However, as written, the upgrade is only a sketch and the specific claim of 'ZK in the usual sense' is not backed by a working standard-model simulator. The central Section 2 results are sound and worth publishing, but the paper's advertised stronger contribution needs substantial additional work.

major comments (3)

[Section 3] The claim that replacing ψ_n by τ(g_s)^b yields ZK 'in the usual sense' is unsupported. In the proof of Theorem 2.2, the simulator C_m is built using an assignment v* with ¬ψ_m(v*)=1 supplied by a nonstandard model M*; the dummy witness is (0,v*). For τ(g_s)^b with b outside Rng(g_s), the formula τ(g_s)^b is a tautology, so ¬τ(g_s)^b has no satisfying assignment in any model, standard or nonstandard. Thus the dummy-witness strategy cannot be realized. The hardness Claim only asserts that such tautologies have no short propositional proofs; it does not give the simulator a falsifying assignment, nor does it provide a way to sample b inside Rng(g_s) while preserving the CRS distribution. No alternative standard simulator is described. The implication from the hard-generator assumption to usual-sense ZK is therefore not established. The author should either supply an explicit standard simul
[Section 3] The load-bearing Claim that a random s makes g_s hard for all pps is imported from the author's own [11] and stated without proof. Since this Claim is essential for the proposed transformation to genuine ZK, the manuscript should either prove it or give a precise theorem statement and reference. Moreover, the use of a shared random string (s,s') changes the setting: the p-time sequence Ψ is no longer fixed, and the definition of ZK relative to T (Definition 2.1) or its CRS analogue is not reformulated. Before the 'usual sense' claim can be evaluated, the author must define the CRS-based ZK notion and state exactly which hardness and NIWI assumptions are needed in that model.
[Theorem 2.2] The proof of Theorem 2.2 establishes only the consistency of the existence of a simulator, not the existence of a standard algorithmic simulator. This is explicitly built into Definition 2.1 and is not in itself a defect. However, the paper's abstract and Section 3 use the phrase 'genuinely zero-knowledge proofs' for the CRS-based construction, creating a risk of conflating the two notions. A revised version should carefully separate 'ZK relative to T' from 'usual ZK' and avoid implying that Theorem 2.2 by itself yields a standard simulator.

minor comments (4)

[Throughout] There are several typos: 'can be turned it into' should be 'can be turned into'; 'form proof complexity' should be 'from proof complexity'; 'termedeffectively ZKin' has a spacing issue. The word 'Gödel' in reference [4] is misspelled.
[Lemma 2.3] Lemma 2.3 is cited rather than proved. The argument is standard, but since the lemma is used in Theorem 2.4, it would be helpful to include a proof sketch or a precise statement with page/claim references from [12] or [7].
[Section 3] The symbol m is used both for the generator stretch (m=2n) and, in the proof of Theorem 2.2, for a nonstandard element. This is confusing. Use different letters for the generator stretch and the model element.
[Section 2] The notation '1(m)' and 'n' for dyadic numerals is introduced in Section 1 but used in the proof of Theorem 2.2 without a reminder. A short sentence recalling that '1(m)' is the dyadic numeral for m would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main theorems are genuine derivations; Section 3 has an unproved jump but not a circular one.

full rationale

The derivation chain is not circular. Definition 2.1 defines ZK relative to T purely by a lower bound on T-proofs of the nonexistence of a simulator; it does not quantify over statements S and does not contain 'indistinguishable from true.' Theorem 2.4 derives the latter using Lemma 2.3 and the defining lower bound: a short proof of (∃C Sim_c(n,C))→S(n) plus the short proof of ¬S(n) (when S(n) is false) would assemble a short T-proof of ¬∃C Sim_c(n,C), contradicting Definition 2.1. This is a genuine implication, not an equivalence-by-construction. Theorem 2.2 is likewise a deduction from the external K-P theorem, the NIWI axioms added to T*, and the hardness of Ψ for P(T*); the nonstandard simulator C_m is exactly the consistency object required by Definition 2.1, and no fitted parameter is renamed as a prediction. The Section 3 upgrade to 'usual-sense' ZK is asserted via a construction from the author's prior [11]; while this is a load-bearing self-citation for that advertised upgrade, the cited Claim has stated assumptions (demi-bit hardness) that do not include the target ZK conclusion and is based on external results [5,15], so it does not make the argument circular. The real weakness is that the paper sketches, rather than proves, that the hard-generator protocol has a standard PPT simulator; that is an omitted proof / correctness gap, not a circular reduction. No step of the form 'X is defined in terms of Y' or 'fitted parameter called prediction' occurs.

Assumptions & free parameters 3 free parameters · 6 assumptions · 0 invented entities

The central claim rests on conjecture-level assumptions, not on fitted parameters: the NIWI existence assumption, the hard-tautology-sequence assumption Ψ (equivalent to non-existence of an optimal pps), and — for the Sec. 3 upgrade — the hard-generator/demi-bit conjecture. The free-parameter ledger contains only existential proof-size constants (d, a) standard to complexity statements, plus the hand-set stretch m=2n in the Sec. 3 construction. No data are fit anywhere; the paper's contribution is definitional and conditional.

free parameters (3)

d — simulator size exponent (Def. 2.1, Thm. 2.2) = existential, uncomputed
Existential constant bounding simulator circuit size (|C| ≤ n^d). Standard complexity-theoretic existential, not fitted to data.
a — proof-size exponent in Lemma 2.3 = existential, uncomputed
Comes from Σ^b_1-completeness; the lemma is cited from [12,7] rather than proven here. Existential constant, no data fitting.
generator stretch m = 2n (Sec. 3) = m = 2n
Hand-chosen parameter for the demi-bit construction, deliberately relaxed from [11]'s m = n + ⌈log n⌉ + 1 to weaken the stretch assumption. Chosen by hand, hence listed.

assumptions (6)

domain assumption (Th): T is a true theory in the language of bounded arithmetic S2, contains S^1_2, and its axioms are p-time decidable
Sec. 1; frames every result in the paper; the author notes the language requirement is inessential.
domain assumption A,B is a non-interactive witness-indistinguishable (NIWI) proof system
Sec. 1; external cryptographic primitive carried from Ilango [4]; T* is true only if a NIWI exists.
ad hoc to paper Ψ is a p-time sequence of tautologies hard for P(T*)
Sec. 1/2; the central conjecture-level input, equivalent to non-optimality of every pps; no construction known (Sec. 3).
domain assumption Existence of a generator hard for all pps / demi-bits of super-polynomial hardness
Sec. 3; needed for the genuine-ZK upgrade; called 'a central conjecture of the theory' by the author; attributed to [5,15,16].
standard math Krajicek–Pudlak Theorem 1.1 linking P(T) non-provability to model extensions
Recalled in Sec. 1; used as a black box in the proof of Thm. 2.2.
standard math Σ^b_1-completeness provable in S^1_2 and the overspill principle
Used in Lemma 2.3 and to convert non-standard m to 'all but finitely many n' in Thm. 2.2 and Def. 2.1.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A proof complexity perspective on effectively zero-knowledge proofs." pith.science (2026). https://pith.science/paper/CFFQI4MN

@misc{pith2026260713540,
  author       = {Pith},
  title        = {Pith review of: A proof complexity perspective on effectively zero-knowledge proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CFFQI4MN}},
  note         = {Machine review of arXiv:2607.13540}
}

read the original abstract

Ilango (FOCS 2025) invented effectively zero-knowledge proofs, a new variant of zero-knowledge. We reformulate it in the language of logic and give simple proofs (under the same assumptions as Ilango (FOCS 2025)) of its existence and of the key property defined in Ilango (FOCS 2025) that it is "indistinguishable from true" (that property is in Ilango (FOCS 2025) a part of the definition of the prover, not its consequence). Using the theory of proof complexity generators we show that the concept can be turned it into a genuinely zero-knowledge proofs, assuming a conjecture from the theory about the existence of a hard generator and allowing the parties to share a common random string.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references · 1 linked inside Pith

[11]

Kraj ´ ıˇ cek, Failure of the strong feasible disjunction property, submit- ted (2025)

J. Kraj ´ ıˇ cek, Failure of the strong feasible disjunction property, submit- ted (2025). ArXiv: 2604.04830v2

arXiv 2025
[1]

S. R. Buss,Bounded Arithmetic. Naples, Bibliopolis, (1986)

1986
[2]

S. A. Cook and J. Kraj ´ ıˇ cek, Consequences of the provability ofN P⊆ P/polyJ. of Symbolic Logic,72(4), (2007), pp.1353-1371

2007
[3]

S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems,J. Symbolic Logic,44(1), (1979), pp.36-50

1979
[4]

R. Ilango, G¨ odel in Cryptography: Effectively zero-knowledge- Knowledge Proofs for NP with No Interaction, No Setup, and Perfect Soundness, in:IEEE 66th Annual Symposium on Foundations of Com- puter Science (FOCS), (2025), pp.1102-1129

2025
[5]

Ilango, The Oracle Derandomization Hypothesis is False (And More) Assuming No Natural Proofs,Electronic Colloquium on Computational Complexity, Report No.190, (2025)

R. Ilango, The Oracle Derandomization Hypothesis is False (And More) Assuming No Natural Proofs,Electronic Colloquium on Computational Complexity, Report No.190, (2025)

2025
[6]

Khaniki, Jump operators, Interactive Proofs and Proof Complex- ity Generators, in:Proc

E. Khaniki, Jump operators, Interactive Proofs and Proof Complex- ity Generators, in:Proc. 65th Annual Symposium on Foundations of Computer Science(FOCS 2024), (2024), pp.573-593

2024
[7]

Kraj ´ ıˇ cek,Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, (1995)

J. Kraj ´ ıˇ cek,Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, (1995)

1995

Show all 16 references

[8]

Kraj ´ ıˇ cek, On the computational complexity of finding hard tau- tologies,Bulletin of the London Mathematical Society,46(1), (2014), pp.111-125

J. Kraj ´ ıˇ cek, On the computational complexity of finding hard tau- tologies,Bulletin of the London Mathematical Society,46(1), (2014), pp.111-125

2014
[9]

Kraj ´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Applications, Vol.170, Cambridge University Press, (2019)

J. Kraj ´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Applications, Vol.170, Cambridge University Press, (2019)

2019
[10]

Kraj ´ ıˇ cek,Proof complexity generators, London Mathematical Society Lecture Note Series, No.497, Cambridge University Press, (2025)

J. Kraj ´ ıˇ cek,Proof complexity generators, London Mathematical Society Lecture Note Series, No.497, Cambridge University Press, (2025)

2025
[12]

Kraj ´ ıˇ cek and P

J. Kraj ´ ıˇ cek and P. Pudl´ ak, Propositional proof systems, the consistency of first-order theories and the complexity of computations,J. Symbolic Logic,54(3), (1989), pp.1063-1079. 10

1989
[13]

Kraj ´ ıˇ cek and P

J. Kraj ´ ıˇ cek and P. Pudl´ ak, Propositional provability in models of weak arithmetic, in:Computer Science Logic (Kaiserlautern, Oct. ’89), eds. E. Boerger, H. Kleine-Bunning and M.M. Richter, Lecture Notes in Computer Science440, (1990), pp. 193-210. Springer-Verlag

1990
[14]

Pudl´ ak, Incompleteness in the finite Domain,Bull

P. Pudl´ ak, Incompleteness in the finite Domain,Bull. Symbolic Logic 23(4), (2017), pp. 405-441

2017
[15]

H.Ren, Y.Wang, and Y.Zhong, Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits, in:Innovations in Theoretical Computer Science(ITCS 2026), to appear

2026
[16]

Rudich, Super-bits, demi-bits, and N P/qpoly-natural proofs, in: Proc

S. Rudich, Super-bits, demi-bits, and N P/qpoly-natural proofs, in: Proc. of the 1st Int.Symp. on Randomization and Approximation Tech- niques in Computer Science, LN in Computer Science, Springer-Verlag, 1269, (1997), pp.85-93. 11

1997

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.

[1] [11]

Kraj ´ ıˇ cek, Failure of the strong feasible disjunction property, submit- ted (2025)

J. Kraj ´ ıˇ cek, Failure of the strong feasible disjunction property, submit- ted (2025). ArXiv: 2604.04830v2

arXiv 2025

[2] [1]

S. R. Buss,Bounded Arithmetic. Naples, Bibliopolis, (1986)

1986

[3] [2]

S. A. Cook and J. Kraj ´ ıˇ cek, Consequences of the provability ofN P⊆ P/polyJ. of Symbolic Logic,72(4), (2007), pp.1353-1371

2007

[4] [3]

S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems,J. Symbolic Logic,44(1), (1979), pp.36-50

1979

[5] [4]

R. Ilango, G¨ odel in Cryptography: Effectively zero-knowledge- Knowledge Proofs for NP with No Interaction, No Setup, and Perfect Soundness, in:IEEE 66th Annual Symposium on Foundations of Com- puter Science (FOCS), (2025), pp.1102-1129

2025

[6] [5]

Ilango, The Oracle Derandomization Hypothesis is False (And More) Assuming No Natural Proofs,Electronic Colloquium on Computational Complexity, Report No.190, (2025)

R. Ilango, The Oracle Derandomization Hypothesis is False (And More) Assuming No Natural Proofs,Electronic Colloquium on Computational Complexity, Report No.190, (2025)

2025

[7] [6]

Khaniki, Jump operators, Interactive Proofs and Proof Complex- ity Generators, in:Proc

E. Khaniki, Jump operators, Interactive Proofs and Proof Complex- ity Generators, in:Proc. 65th Annual Symposium on Foundations of Computer Science(FOCS 2024), (2024), pp.573-593

2024

[8] [7]

Kraj ´ ıˇ cek,Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, (1995)

J. Kraj ´ ıˇ cek,Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol.60, Cambridge University Press, (1995)

1995