The Blue Eyes Puzzle: Thinking About What Others Know

Some puzzles test your memory. This one tests whether you can think about what other people are thinking. The Blue Eyes puzzle has a reputation for stumping smart people. This piece explains what the puzzle is about, shows the kind of reasoning it demands, and points to a machine-checked solution.

What the Puzzle Asks

The puzzle comes from Randall Munroe, the xkcd author. The Archive of Formal Proofs entry summarizes the setup this way:

Perfect logicians, forbidden from communicating, are stranded on an island. They may leave once they have figured out their own eye color. (Paraphrase of the Archive of Formal Proofs entry.)

That is the core. Nobody can be told the answer. Each logician works only from what they can observe and what they can deduce.

One limit to state plainly. The sources behind this piece do not give the full original wording, the number of logicians, or the exact eye-color rules. So this is not a puzzle you can solve here from a verified statement. Read Munroe's original text for that. What follows is an explainer on the reasoning and on the proof that checks it.

A Warm-Up in Reasoning About Others

To feel the skill involved, try a toy case of my own. It is not Munroe's wording and it is not drawn from the sources. It only shows the style of thinking.

Imagine two perfect logicians. Each can see the other's eye color but not their own. Suppose each knows that a certain rule holds, and each knows the other knows it. Now one logician looks across and sees a person who has the trait in question. That tells them nothing about themselves yet. They wait and watch what the other does.

Here is the move. If the other person does not act when they would have if they could see nothing special on you, then your own trait is the missing piece. Silence becomes information. You learn from what a perfect reasoner fails to do.

That is the heart of this family of puzzles. You are not only asking what you know. You are asking what each person knows, and what they know about what you know. You build a small model of another mind and run it forward one step at a time.

Why Common Knowledge Matters

Logicians have a name for the group version of this idea: common knowledge. A fact is common knowledge when everyone knows it, everyone knows that everyone knows it, and so on without end. The Stanford Encyclopedia of Philosophy has an entry on it, and a preview page points to it.

I can't quote that entry, though. The preview shows only access and site text, and the content sits behind a login. So treat the link between common knowledge and this puzzle as background worth reading, not something I can cite from that page.

The general point stands without it. Reasoning about layers of knowledge is hard because each layer adds a step. Perfect logicians on an island have no trouble with that. People do.

A Formal Solution, Checked by Machine

Here is where skeptics get something solid. Maya Kądziołka published a formal solution, dated January 30, 2021, in the Archive of Formal Proofs. According to the entry, it models the behavior of perfect logicians and formalizes the solution in the theorem prover Isabelle. The entry is filed under Logic/General and Logic/Logics of knowledge and belief.

What does that buy you? A theorem prover is a program that checks each step of an argument. You don't have to trust the author's cleverness. The machine either accepts the proof or it doesn't.

The venue adds weight. The Archive of Formal Proofs is organized like a scientific journal. It is indexed by dblp, carries ISSN 2150-914x, and its submissions are refereed. So the result has both machine checking and human review behind it.

Another caution. The pages I have do not lay out the reasoning steps or state the final answer in prose. I can tell you the proof exists and how it was vetted. I can't walk you through it from these sources.

How to Read It Yourself

If you want to go deeper, here is a sensible order.

1. Read Munroe's original statement so you have the exact rules.
2. Try the smallest versions first, as in the two-person warm-up above.
3. Ask at each step what a perfect logician could conclude, and what the others could conclude about them.
4. Only then open the formal proof and compare it with your own reasoning.

You will learn more from being wrong first than from reading a solution cold. And when the proof is hard to follow, that is normal. Isabelle does not skip steps that a person would wave away.