Are there 3-colorable maps that can never be colored? I just watched this explanation of zero-knowledge proofs with Avi Wigderson: https://www.youtube.com/watch?v=5ovdoxnfFV
Key claims from the video:

Every formal statement can be translated into a map in a way that preserves truth. If a statement is true, its map will be 3-colorable. If not, it isn't 3-colorable https://youtu.be/5ovdoxnfFVc?t=1721

If every formal statement can be translated to a map, and suppose there's a true statement that can't be proven true by Gödel's incompleteness theorems, then doesn't that mean that no algorithm whether P, NP, or worse can exist to color it? Does that mean that there are some 3-colorable maps that can never be colored?
This seems wildly counterintuitive (which maybe is just the nature of Gödels' incompleteness theorems, which I haven't tried to understand the proof of). Or maybe I don't understand Gödel's incompleteness theorems (also likely). If I'm misunderstanding something though, it'd be helpful to know what to look into more.
Every formal statement can be translated into a map in a way that preserves truth. If a statement is true, its map will be 3-colorable. If not, it isn't 3-colorable https://youtu.be/5ovdoxnfFVc?t=1721

Every formal statement in propositional logic can be translated to a map 3-coloring instance. The video is being very sloppy with calling this 'every mathematical statement', as there's many mathematical statements that aren't captured in propositional logic.
Propositional logic is decidable (it's equivalent to the SAT problem).