Spark & Anvil Privacy

Proof cases

Nine people, one decision each — what makes a step a proof, and what does not.

A case · you decide

Theo and the line he did not prove

Theo — a 16-year-old who wants to prove everything, including where the proof starts

The idea in play: a given — every proof starts from facts it accepts without proof (here: the opening is safe).

Line 0 of every Proof Sweeper board reads “Given: the opening is safe.” Theo asks why that line needs no rule.

Every later line cites a rule and some numbers. Those numbers only exist because the opening was revealed.

Something has to come first, or there is nothing to cite.

What is line 0?

Start a proof →

A case · you decide

Amara cites the done rule

Amara — a 15-year-old writing her first accepted proof line

The idea in play: the done rule as a citation — one premise number that already touches all its proven mines.

Amara wants to open C4. Next to it is a 1 at B3, and B3 already touches one proven mine.

The board asks for three things: the claim (safe), the rule (done) and the premise (B3=1).

If any of the three is wrong, nothing opens.

What does the accepted line say?

Cite a done step →

A case · you decide

Felix and the only places left

Felix — a 17-year-old who can see mines but struggles to justify them

The idea in play: the full rule as a citation — a number whose hidden squares are exactly its missing mines.

A 3 at E5 has three hidden neighbours left and no proven mines yet. Felix knows all three are mines.

He writes “E6 is a mine — by full (E5=3)” and it is accepted.

He tries the same citation for a fourth square, F7, which touches a different number.

Why is the F7 line rejected?

Cite a full step →

A case · you decide

Yuki and the order of the premises

Yuki — a 16-year-old stuck on the first board that needs the subset rule

The idea in play: the subset rule takes two premises, the smaller set first — the one whose squares sit inside the other’s.

Yuki sees that the hidden squares of a 1 at D2 are all among the hidden squares of a 2 at D3.

She submits “subset (D3=2, D2=1)” and the board explains that the smaller set comes first.

The rule reads: the squares the 1 touches are inside the squares the 2 touches.

How should the citation be written?

Cite a subset step →

A case · you decide

Omar and the flag he only believed

Omar — a 17-year-old who flags by instinct in ordinary Minesweeper

The idea in play: proven ≠ flagged by hunch — only a mine proven by a cited step can be used as a premise.

Omar is sure G2 is a mine. He wants to use it to prove its neighbours safe with the done rule.

His citation is rejected: G2 is not a proven mine yet, so the number next to it still has a mine unaccounted for.

He is probably right about G2. Probably is not enough for a proof.

What should Omar do?

Prove before you flag →

A case · you decide

Beatriz and the rejection that helped

Beatriz — a 15-year-old who hears “wrong” as “you are bad at this”

The idea in play: a rejected step says what the premise still needs — feedback about the argument, not the person.

Beatriz’s step is rejected. The message says the 2 at C5 still has two hidden squares that could hold its missing mine.

Her first instinct is to close the tab.

Then she reads it again: it tells her exactly which fact is missing.

What is the most useful way to read the message?

Read why a step was rejected →

A case · you decide

Sven and the board you cannot lose

Sven — a 16-year-old who tries to trick the board into opening a mine

The idea in play: soundness — a step that passes the checker can never be false, so a proof can never hit a mine.

Sven keeps trying citations that are nearly right, hoping one slips through and opens a mine.

Every one is rejected, and nothing on the board changes when a step is rejected.

The checker never looks at where the mines really are. It only checks whether the rule and the numbers force the claim.

Why can a Proof Sweeper game never be lost?

Try to lose a proof →

A case · you decide

Zara and the level that measured itself

Zara — a 17-year-old designing puzzles for her school’s maths club

The idea in play: difficulty is measured, not assumed — each tier’s boards are checked to need the rule they teach.

Zara wants a board that forces people to use the subset rule. Her hand-made boards keep turning out easy.

Proof Sweeper builds a board, then solves it with a perfect logician and counts how many subset steps were needed.

A board that needs none is thrown away for the Proof tier. The Hard tier needs at least three.

How should Zara check her own boards?

Pick the Proof tier →

A case · you decide

Nikhil and the numbered lines

Nikhil — a 16-year-old whose written maths loses marks for missing steps

The idea in play: a proof is a chain — each numbered line cites facts established on earlier lines.

When Nikhil clears a board, Proof Sweeper shows his proof: twenty numbered lines, each citing a rule and numbers.

Line 12 uses a mine proven on line 9. Line 9 used a square opened on line 4.

Nothing on line 12 would make sense without the lines above it.

What makes the written proof trustworthy?

Read your proof →

When two ideas meet

Two cases where two people’s rules work together — one proof feeding the next.

A case · you decide

Amara and Omar: prove the mine, then cite it

Amara & Omar — a first-time prover whose done step keeps being rejected, and a friend who never uses a hunch as a premise

The idea in play: a proof builds forward — the done rule can only rely on mines that earlier lines have already proven.

Amara writes “C4 is safe — by done (B3=1).” The board rejects it. B3 does touch a mine, she is sure of it.

Omar asks where that mine was proven. It was not: Amara can see it, but no line says so.

A 2 elsewhere has exactly two hidden neighbours, one of which is B3’s mine.

What should Amara write first?

Write the two lines →

A case · you decide

Nikhil and Felix: the link that does not connect

Nikhil & Felix — a student who sees a proof as a chain, and a friend who learned where each premise’s reach ends

The idea in play: each line of the chain must be checkable from the lines above — and a premise number only speaks about its own neighbours.

Nikhil reads a friend’s proof. Line 6 says “E7 is safe — by done (B3=1)”. Every line above it was accepted.

Felix counts: E7 is three columns away from B3. It is not one of B3’s neighbours.

So line 6 is not checkable from the lines above, however good they are.

What is wrong with line 6?

Check a chain →