OP: Although I'm not really in the target audience for this demo (I already knew all the punchlines), it does occur to me that it might be helpful to readers like the parent-commenter — and even perhaps thought-provoking to us know-it-alls — if you provided a mode at the end of the demo where the graph was in fact not three-colorable, and the computer actually would lie about its being three-colorable. So it would generate a "three-coloring" with a flaw somewhere, and display its representation as products of primes, and you'd get to choose two adjacent products and receive their factors... and so you could see for yourself exactly how long it took for you to luck into catching the computer in one of its lies.
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.)
For me it was less about the idea of how likely you'd quickly it converges to you almost certainly outing them vs misunderstanding the idea that a zero knowledge proof is about, more or less, the "limit" of the validation behavior to an arbitrary point choosable by the tester not necessarily an actual guarantee you can finitely reach the conclusion.
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.
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!)