Graph associated to a mathematical statement (for the purpose of zero-knowledge proofs)

Question

I'll preface this question by saying I have very little (zero!) knowledge of theoretical computer science, and this post is a genuine attempt to understand something, even if at an intuitive level, which lies quite far from the field in which I work. Please forgive the amateurish wording and feel free to edit as appropriate.

In this numberphile video from several months ago, Avi Wigderson explains the idea behind this 1991 paper of his with Goldreich and Micali in layman terms: define a mapping from mathematical statements to graphs, such that every 3-coloring of the output corresponds to a proof of the input. As an abstract example, he gives Fermat's last theorem (FLT), whose statement happens to be very simple one in Peano arithmetic but is very difficult to prove.

The paper, however, says that the mathematical statement must lie in NP (and also mentions CNF formulas). The only way I can think of of transforming FLT into a decision problem is something along the lines of $\not \exists x,y,z,n \in \mathbb N, \ n > 2, \ x,y,z,n \leq M \ x^n + y^n = z^n$ where $M \in \mathbb N$ is the input. While this is obviously in coNP, I cannot see why it should be in NP (what's a certificate for $M$?). Also, this should be proved for all $M$, so does this mean the resulting graph would have to be infinite? And finally, if the graph has infinite edges, I don't see how the zero-knowledge mechanism can work with arbitrary accuracy, since I could have a faulty proof that yields a colouring which fails on finitely many edges, and I would get caught with zero probability (at least if each check only consists of one/finitely many edges as described in the video).

I get that FLT is mentioned a little tongue-in-cheek, and perhaps I'm taking the claim a little too literally, but I also find it strange that Wigderson would make it without issuing any sort of caveat if it is indeed the case that the paper only applies to formulas involving only $\neg, \vee, \wedge$. I would be very grateful if someone familiar with this material could clear up my confusion.

Answer 1

The $NP$-problem here is not the problem of finding y,z,n, but rather the following problem: "Given a mathematical statement $A$ that can be encoded in $n$ bits, does there exist a proof of $A$ in Peano arithmetic that can be encoded in $p(n)$ bits?" where $p$ is some arbitrary fixed polynomial and the particular encoding is chosen in advance.

This problem is clearly an $NP$-problem, since it is possible to design a polynomial-time Turing machine that takes as an input $A$ and a candidate proof $P$, and says accepts iff $P$ is a valid proof of $A$. Therefore, there is a way to map every statement $A$ into a graph $G(A)$ that is $3$-colorable iff $A$ has a proof of length at most $p(n)$.