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

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.

• (1) The transformation in question is not of FLT into a decision problem, but the proof of FLT into one. That is, $L$ is the set of all (encodings of) valid mathematical statements for which there exists a (standard) proof of length bounded by some fixed polynomial in the statement length, and we want to find out if $x\in L$ where $x$ is an encoding of the statement of FLT. (2) I don't think any reduction should have infinite edges since it takes place in polytime. As long as it's polynomial, a (different) polynomial number of color reshufflings and edge queries can get you to 1-ɛ soundness. Dec 24 '21 at 21:27
• Thanks for your comment. Maybe I misunderstood the video then: I thought he was defining (roughly speaking) mappings $G \colon \{\text{mathematical statements}\} \to \{\text{graphs}\}$ and $P_s \colon \{\text{proofs of } s\} \to \{3\text{-colorings of } s\}$ for statements $s$. If $G(\text{FLT})$ were a finite graph, this would mean we can check whether it holds true through a finite search, which seems very strange. What am I getting wrong? Dec 26 '21 at 9:54