Schrödinger’s Hats: A Puzzle about Parities and Permutations

Meet Schrödinger, who travels the world with an unusually clever clowder of n talking cats. In their latest show, the cats stand in a line. Schrödinger asks a volunteer to take n+1 hats, numbered zero to n, and randomly assign one to each cat, so that there is one spare. Each cat sees all of the hats in front of it, but not its own hat, nor those behind, nor the spare hat. The cats then take turns, each saying a single number from the set {0..n}, without repeating any number said previously, and without any other communication. The cats are allowed a single incorrect guess, but otherwise every cat must say the number on its own hat.

In this talk, we’ll methodically derive a solution, and we’ll formally prove that the method always works. Along the way, we’ll reinvent some elementary theory of permutation groups, in particular, a parity property. You’ll get a taste of what it’s like to formally model a problem in Isabelle/HOL, and prove properties of interest. This is the same theorem prover we use to prove the functional correctness of the seL4 microkernel.

For more information on the topic, see the GitHub repository.


Target Audience

developers, Technical leads and Architects,programmers, testers, business analysts and product owners,programmers, testers, business analysts and product owners and product owners


schedule Submitted 1 year ago