Proof Sweeper
Every square you open has to come with a reason. You can’t lose — you can only prove.
📜 Prove a board →Three rules of inference
- done. A number already touches all its mines → its other hidden neighbours are safe.
- full. A number’s undecided neighbours are exactly the mines it still needs → they are all mines.
- subset. Number A’s undecided squares all sit inside number B’s → B’s extra squares hold exactly (B’s missing mines − A’s): if that’s 0 they are safe; if it equals their count, they are mines.
Circuit levels
In 2000 Richard Kaye showed Minesweeper consistency is NP-complete by building boards that behave like logic circuits — “wires” that carry a true/false value and “gates” that combine them. Proof Sweeper has four of them: a wire, a NOT gate, an AND gate and an OR gate. You are given the inputs, and you prove what the output must be.
A real case · you decide
A case: Lucia and the word “obviously”
Lucia — a 17-year-old whose geometry teacher keeps writing “why?” in the margin
Lucia is quick at Minesweeper. Her teacher bets her she can’t clear a board if every move has to be justified in writing.
The first moves are easy: a 1 with only one hidden neighbour means that neighbour is a mine. She writes it down — rule full, premise B2=1.
Then she reaches a spot where she just “knows” D4 is safe. The checker asks for the premise. She has to stop and find it.
D4 feels safe. What does she write?
No single number decides the next square. What now?
She won the bet. The margin note she kept was the last line of the proof: every claim, a reason.