Echo
Play Echo.
It is a proof engine.
Echo is a puzzle game that is also a real, shared proof-search engine. You recolor small graphs to clear "bad shapes"; every solve that lowers the count on an open math problem becomes a permanent move in a proof tree that a SAT solver closes off. The same engine runs several problems - you pick which board to play.
The system
01A proof search you can play
Each problem Echo runs is the same kind of object: a way to color the connections of a complete graph so that no forbidden "bad shape" (a clique that is all one color) appears. The full graph is far too big to color by hand, so Echo turns the search into a stream of small, readable puzzles and stitches the answers back together.
The whole machine is one loop, repeated by everyone, forever:
-
You get a small piece
The server cuts a small induced slice out of the current best coloring - a dozen or so nodes with a few bad shapes and a handful of edges you may recolor. The rest is locked.
-
You clear the bad shapes
Recolor the flippable edges until the bad shapes are gone. It plays like a clean logic puzzle. Crucially, the server only ever hands you a piece whose solution also lowers the count on the whole graph - so clearing it is never a local trick, it is real progress.
-
Your colors are committed
Your edge colors are replayed on the server and, if they strictly lower the full-graph bad-shape count, committed as a new branch of a shared proof tree. The next player builds on top of your branch.
-
A solver settles branches
As branches accumulate decisions, a SAT solver (the kind used in formal proofs) asks the exact question: can this be finished with zero bad shapes? It either finds the finished coloring (a win) or proves the branch is a dead end (exhausted).
What you actually do
02The game in one screen
You are shown a small graph. Some edges glow as bad cliques - the shapes we want gone. You can recolor a handful of highlighted edges; the rest are locked. Each move must leave strictly fewer bad shapes than before. Clear them and the puzzle is solved.
It feels like a self-contained logic puzzle, but it is not a simulation. Every edge color you see is a real edge color in a real research graph, and every locked edge is a decision the search has already made or a structure already proven clean.
Why a solve is real progress
03From your solve to the proof tree
The hard part of this kind of search is that fixing one corner of a graph can quietly break another. So Echo never serves a puzzle blindly: before a piece is offered, the engine checks that clearing it lowers the bad-shape count of the entire graph, not just the slice you see. That is what makes every served puzzle a genuine step.
When you solve one, your committed colors become a new branch, and the lowest count any live branch has reached is the network's record - a number that only ever ratchets down. Branches grow in two directions at once:
How a branch ends
04The two outcomes that matter
Once a branch has enough decisions, the SAT solver asks one exact question: given these committed colors, is there any way to finish with zero bad shapes? Two answers matter, and they push in opposite directions. Both are progress that never resets.
YES, here it is
The solver returns an actual clean coloring of the whole graph. That coloring is a proof of a new lower bound. The board is won. This can happen on any branch, at any time.
NO way
That branch is a dead end. Its whole subtree retires and that slice of the search space is permanently eliminated. The explored fraction only ever grows.
The same engine handles any such problem - any graph size, any number of colors, and even different forbidden shapes per color (so it covers symmetric and asymmetric problems alike). Adding a new problem is a config entry plus a starting coloring; the loop above is unchanged.
The problems
05What you can play
The targets are Ramsey numbers: the size at which a coloring with no bad shape becomes impossible. Driving a board's count to zero proves a lower bound on its Ramsey number. We run three, deliberately chosen to be honest about what is winnable. Each has its own accent in the app; you switch between them from the home screen.
R(4,4) ≥ 18 · practice
Two-color 17 nodes with no single-color group of 4. Solved since 1955, so a clean coloring provably exists and the dial really reaches zero. The proving ground - where you see the whole engine work end to end, and the best place to start.
R(4,6) ≥ 37 · frontier
Two-color 36 nodes with no red group of 4 and no blue group of 6 - an asymmetric board. It is open (36 ≤ R(4,6) ≤ 40), and off-diagonal bounds like this still get pushed, so reaching zero would set a genuinely new record.
R(5,5) ≥ 44 · legendary
Two-color 43 nodes with no single-color group of 5. Open and unmoved in decades (43 ≤ R(5,5) ≤ 46). Reaching zero may not even be possible, so the prize here is the record the network drives down together.
live from the running search
On R(5,5) the engine uses a known head start: in 1997 McKay, Radziszowski and Exoo enumerated the 656 perfect colorings of 42 nodes. Echo locks one of those proven-clean cores, attaches a 43rd node, and lets players color only the new node's edges - so your choices are exactly the conjecture's open variables. R(4,4) and R(4,6) instead start from a full near-clean coloring and let the whole graph move.
Straight talk
06Is this real, or a gimmick?
It is real, and we stay honest about exactly how. The starting graphs are genuine catalogue data. The locked edges are genuinely locked. Branch closure is real UNSAT exhaustion from a standard SAT toolchain, checked against known answers like R(3,3) = 6 and R(3,3,3) = 17.
We are also honest about what can be won. R(4,4) is winnable - a clean coloring exists, so the search genuinely finishes. R(4,6) is open but improvable - reaching zero would be a real new record. R(5,5) likely cannot be won this way - most believe no clean 43-node coloring exists, so the number that matters is the lowest the network has ever reached, a record that only ratchets down. The point is a system where ordinary play accumulates, never resets, and lets anyone touch a real open problem.
Support
07Keep the search running
Echo is not a typical game. Every solve triggers real computation on a cloud backend: SAT-based branch closure plus a proof tree that never resets. That compute carries a monthly bill, and it grows as more people play.
If you would like the search to keep running, you can chip in. One coffee covers a chunk of the server bill, and all of it goes straight to infrastructure. No ads, no paywalls, no tracking. The game stays completely free either way.