The proof engine, animated.

One looping picture of the whole game, on a real board. The graph below is an actual R(4,4) colouring - 17 nodes, two edge colours, drawn from the Paley graph - carrying five "bad shapes" (cliques that are all one colour). Echo lifts one out as a small puzzle - the four-node bad shape plus three locked context vertices - you recolour the single off-colour edge to clear it, and your colours commit back as a new branch of a shared proof tree. Then a SAT solver settles that branch - it finds a clean colouring (SAT, a win), proves it impossible (UNSAT, exhausted), or leaves it open to explore. Nothing ever resets.

R(4,4) - the real 17-node board (Paley graph) · lift a bad shape out → clear it → commit → grow the tree → the SAT solver closes, exhausts, or leaves it open

red / blue edges - the two colours the edge you recolour to clear a bad shape open: a live branch the SAT solver hasn't settled SAT: the solver found a clean colouring - a win UNSAT: the solver closed the branch - exhausted

Play Echo on the App Store How the system works