I recently watched a video on Numberphile2 in which Avi Wigderson describes how one can prove a graph has a 3-colouring in zero-knowledge and that as 3-colouring is NP-complete, all NP statements have zero-knowledge proofs. He further emphasises that this is constructive; one can turn a proof of an NP statement into a zero-knowledge proof of that statement.
As I already understood the Cook-Levin reduction from NP problems to 3-SAT and the reduction from 3-SAT to 3-colouring, I thought I'd be able to do exactly this with a simple mathematical statement like the infinitude of the primes, but I seem to be missing some steps in the process.
I should first say that my understanding is that the statements which are in NP are precisely the statements which have a second-order formula only involving existential second-order quantification, which certainly seems to cover all the mathematical statements I can think of. For my desired example, one can express the infinitude of the primes with the following second-order formula:
$\exists f \forall x \forall y (x < f(x) \land 1 < f(x) \land (1 \nless y \lor y \nless f(x) \lor y \nmid f(x)))$
It expresses that there exists a function $f: \mathbb{N} \rightarrow \mathbb{N}$ such that the output of $f$ is prime and always produces output bigger than its input, for all natural number inputs, therefore there must be infinitely many primes. And so proving the existence of such a function $f$ constitutes a proof of the statement.
Though it's an awkward way of writing it, it does have the advantage that the predicate being quantified over is in Conjunctive Normal Form, which is what is required for the reduction from 3-SAT to 3-colourability. But I don't understand where to go from here, as the existential quantifier isn't quantifying over predicates (having Boolean outputs), the universal quantifiers are quantifying over natural numbers and the predicate involves two binary predicates on natural numbers $<$ and $|$.
How does one reduce the problem of proving a mathematical statement (second-order formula with no second-order universal quantifiers), such as the infinitude of the primes, to the problem of proving a SAT instance has a satisfying assignment? Preferably in a way that is somewhat good at minimising the size of the resultant SAT instance.
Best Answer
Instead of converting the statement "the primes are infinite", you can convert the statement "there is a proof that the primes are infinite with less than n steps in deductive system X", for some X. This new statement can be more easily converted to SAT and 3-colorability.