There were a lot of fun technical parts to building this:
- For implementation reasons, it’s much easier if the lines all have integer intersection points with each other. To do this, when a new line is added I “cheat” by rounding intersections to integers and then splitting the old lines at the intersection into new linds (with potentially different slopes) going through the rounded point
- I had to draw semi accurate maps of actual places (UK, South America, US west coast) in the HTML canvas using just line segments. I tried a few different solutions, including using SVG data. I ended up using the topojson library to give nice line approximations to GeoJSON maps
- I use a simple backtracking algorithm to handle the live coloring of graphs
- I use turf.js’s polygonize function to handle finding polygons from line segments (very happy I didn’t have to implement this myself!)
- I wanted to make the game as mobile friendly as possible (don’t think I’ve nailed this quite yet)
There were also a few tradeoffs I made:
- I wanted give links earlier in the game for players to learn more, but I decided to wait until the end to maintain the flow of the game
- In order to make the game more mobile-friendly, I generally stuck to maps with a small number of regions (at least for maps people have to interact with them). So for the most part all of the instances in the game are “easy”
Thanks for leading us down this mathematical rabbit hole today.
You could take a piece of paper (much larger than the picture/book), and cut out a waldo-shaped hole it and position the paper such that he is shown in the hole. Then, when you show it to the challenger, they know that you have found him without you revealing where he is.
In a real ZK proof the probability of the prover lying reduces after each iteration but never reached 0.
- The physical demonstrations at 1:16 and 3:48 were helpful
- thinking of proofs as between a prover and a verifier, not as classical deterministic proofs
- insight into the name "zero-knowledge", as in "you can already predict the answer, so you're not gaining any knowledge from that interaction"
[1]: https://en.wikipedia.org/wiki/Heawood_conjecture
So by doing this over and over again, if the two you choose are always different colors, you approach a 100% certainty that it's legit.
You never really get a 100% proof but the more times you repeat the closer you are to being sure. At 99.999999% after repeating this enough times, you'd most likely be satisfied.
The person can just always give two different colors (and never two same colors) when you reveal two post it notes, so you could never proof them false.
Only after re-reading I realized _all_ the colors are to be hidden under the post it notes _beforehand_, not at the time you choose two post it notes.
EDIT: yep looks like it, the leftmost picture under 'snapshots' here is a 2D map of what's on the torus and looking at e.g. the blue band, it touches all 6 others (just barely the cyan and yellow ones with a few pixels of its tips when wrapping between top/bottom): https://demonstrations.wolfram.com/SevenColoringOfATorus/
First, both you and the oracle know what the uncolored map looks like, and what the 3 colors are.
Step 1: The oracle sends the entire 3-colored map, but asymmetrically encrypted. So you can't see the map, but the oracle can't "un-send" it. If no 3-coloration of the map exists, the oracle has to send you something, and because you know what the map and colors look like, the only thing they can send is a map where some two adjacent regions have the same color.
Steps 2&3: You randomly pick two adjacent regions and ask the oracle for their decryption keys, so you can see their colors. When you initially received the encrypted map, you could not know whether it had two same-colored adjacent regions. But, if you happen to randomly choose the same-colored regions, the oracle has no way of not telling you. If the oracle refuses to send the decryption keys for those regions, or sends ones that don't successfully decrypt, you'll know something is up, and can assume the regions are the same color. And the only keys that successfully decrypt the regions' colors, decrypt into their original colors; so the regions will only decrypt into different colors, if they were different colors in the encrypted map the oracle originally sent.
To further illuminate: the "random pick after the map is received" ensures that the oracle must send you a map where all adjacent regions have different colors, even though you can't see all the colors yourself. Otherwise, the oracle can't guarantee that you won't ask for the two regions with different colors (because they sent the map before you randomly pick), and if you do ask for those regions, they can't respond in a way that re-assures you the colors are different (because the only way to do so is send keys that decrypt the regions into separate colors, and since they decrypt into the same color, such keys don't exist).
Step 4: Repeat steps 1-3 an unbounded number of times. This is necessary because in a single iteration, there's a chance that the oracle sends a map with two adjacent same-colored regions, but you pick two different regions; so the map is un-3-colorable, but you don't find out. In fact, this is a very high chance if it's a large map and only a single pair of adjacent regions have the same color. But more iterations increase the probability that you do find out indefinitely; with enough iterations, the probability that one of them you get lucky and select the same-colored region is 99.999...%.
Also, each time you repeat steps 1-3, the oracle sends the map with a different coloration. Otherwise, you'd slowly reveal the colors to get the fully-colored map, so it wouldn't be a zero-knowledge proof (two colors in each of two maps with different colors doesn't give you any more information than two colors in one map, so even with unbounded iterations the original coloration isn't revealed). If the map isn't 3-colorable, the randomization doesn't affect the probability: when the oracle randomizes the map, they could choose an entirely different coloration and give two different adjacent regions the same color, but the probability of you randomly choosing those two regions stays the same, so the probability of "getting lucky" in one of enough iterations also stays the same, at 99.999...%.
I knew that 4 colours sufficed for any arbitrary map from back in the day when I learned this, but still I found it VERY rewarding by attempting to draw a map that needed 5 colors, and how intuitive this demo was for getting a "feel" for a thing that I knew only theoretically! Like I needed an impossible geometry to fit, either an area that stretched to a zero-width path (which would becomes a point, and thus 2 areas, so doesn't fit) or some other "impossible" geometry. Loved it, congrats on a really well executed idea!
https://en.m.wikipedia.org/wiki/Four_color_theorem
It feels like something that got detached from the things that make it work during simplification. Or it could be that I just have a misunderstanding/oversight in the zero knowledge proof :).
In an unrelated note: I colored the larger graph and it didn't even play along!
For the ZK example, the math behind it is this: if there are m bordering regions and I am lying, you have a 1/m chance of catching me each time. Thus after k repetitions the chance you haven't caught me is (1-1/m)^k \approx e^{-k/m} which is extremely small for k sufficiently larger than m.
Now, you may rightfully say: hey that's still not a "proof," you could still be lying! There are two responses to this:
1. The probability can be made incredibly small, like smaller than the the chance, say, your computer got hit by a gamma ray burst that would flip bits from 0 to 1 (I really have no idea if this actually happens but people have said it to me).
2. It turns out it is mathematically impossible to get the zero knowledge property if you want true proofs (i.e., no probability of being wrong). So, there's a trade off: if you want zero knowledge, you have to accept some (small) failure probability
P.S. Adding an easter egg for coloring the larger graph is on the todo list :)
But none of that is telling you how much is "sufficient", or even which order of magnitude we're talking about. If the quantity has a real life cost, this would result in enormous practical differences.
(With the formula you have given for the ZK proof, we're at least one step further: You can start with the desired probability, e.g. the gamma ray burst und calculate the required minimum k from that - also, it's easy to see that the color problem lends itself well to such proofs because the probability of failure drops exponentially quickly with growing k, so the actual k you choose can be relatively small. But if all you have is a proof in the limit, that's not possible)
Looking forward to the easter egg :)
And the demo could also tell you the expected number of iterations to catch the lie with (50/90/99%) probability. It'd be a pretty large number even for such a small graph, I'd bet.
(Of course the computer could also lie about the factorizations, since it's unlikely a human would bother to catch it in that kind of lie; but let's assume it doesn't ever do that.)
Readers might also be interested in the https://mathworld.wolfram.com/McGregorMap.html (reported, on 1 April 1975, to require five colors!)
Prior to this I'd only seen "proof" in math where it has meant you can absolutely guarantee there to bo no counterexample not just that it seems impossibly unlikely there could be a counterexample. E.g. the Tarry-Escott problem where we have proof there is no sets exists with n=4 and m=5 even though we haven't ever found numerical values of sets matching that description or Merten's conjecture where the smallest counterexample is estimated to be so large (~10 billion digits) we've not even been able to find the first counterexample value despite knowing it exists due to a proof. On the other side of things we have things like the Goldbach conjecture or Riemann Hypothesis where we've poured our hearts, brains, and souls into trying to find a counterexample or proof and don't claim to have either yet.
Adjusting to that definition of "proof" for the context it all makes a lot more sense now.
So isn't it possible that there is a polynomial time algorithm for integer factorization, but no polynominal time algorithm for 3-coloring, and therefore the "zero knowledge proof" actually reveals the answer?
However, if P = NP, there is no process that works here - there's nothing that is hard to do but easy to demonstrate, and therefore no zero knowledge proofs exist.
Actually, that's not true either. It requires the definition that all polynomial-time algorithms run quickly and all superpolynomial ones run slowly. This is not an accurate definition for all practical problem sizes and this is where the analogies all break down. Polynomial vs nonpolynomial is more interesting to complexity theorists than "how many years would this actually take with a fast computer".
That's fine though, because the point isn't really to publish math papers without disclosing proofs. For example, presenting a valid digital signature is sometimes colloquially called a proof that you had the private key, even though there is 1 in gazillion chance that you didn't. For such practical tasks, very high chance tends to be good enough.
This confused me at first.
That still leaves how to rely on chance of picks for a proof though.
Many, many people have died for this triviality.
"Somewhat fraught" is a very interesting choice of words, but then again, so is "The Troubles" (when the subject matter is decades of bombings and killings).
Very well done, I'll try to see if my children will enjoy that already too.
I'm happy to find a contact there if you want
> Step 2. You click any two bordering regions, and I pull off their post-its
> Step 3. You check that the revealed colors are different
I would add explicitly in step 1 that you tell me what 3 colors you used, and in step 3 that I check that the revealed colors are different from each other and are both from that set of 3. Similar in the explanation of why this should convince me.
This was so much cooler than just being told that 4 colors is enough for every map – this one will stick with me.
It would be wonderful if schools taught a bit more like this – I almost felt like I discovered it myself!
I understand that you want to emphasize the fact that no human can understand the proof with a full overview, but I wonder whether the current sentence will not make people think mathematicians are not perfectly sure of the proof.
https://github.com/clarus/falso
Proof and belief I think are pretty strongly intertwined, but I'm not going to pretend to have a particularly rigorous philosophy on the matter. Similarly, when the proof of Fermat's last theorem was published, I don't know if I should consider that to be a proof because it is well beyond my comprehension. I have no reason to question it, but should I consider it a proof? I know that people smarter than me (e.g. Wiles) thought the original version of it was a proof, but it had a subtle error in it which required a fix. While I haven't looked at the proof and revision, I would be surprised if I could look at the two versions as labelled and tell which one is the correct version.
Or some such.
To top that up, it's fact that there have been "proves" that were wrong (or maybe that's just my believe? :^]) even for a long time.
Hence, I think we can say that there are 4 options for a theorem:
1) Some mathematician believes the theorem is correct (but can't prove it)
2) Some mathematician believes the theorem is incorrect (but can't prove it)
3) Some mathematician believes the proof of a theorem is correct
4) Some mathematician believes the proof of a theorem is incorrect
Proving that a proof is correct is kind of meaningless. At that point it's all believe anyways.
And those many jobXtoY.v and taskXtoY.v files sure look like they also do the same as the Appel and Haken proof, namely enumerate lots and lots of cases that are then machine-checked. So I don't think the computerized Coq proof is really qualitatively different from other computerized proofs that enumerate so many cases that a manual check would be impractical.