Imagine being handed one rule for an unfamiliar mathematical machine. Feed it any two objects, and it gives you another object; the rule tells you how. Now someone asks a deceptively simple question: does that one rule force a second rule to be true, too? Or can you build a machine that obeys the first while breaking the second?
This is the puzzle behind Georgios Kissas’s Rózsa, a program designed to search for either answer. Its challenge is not just to guess correctly. It must bring evidence: a derivation showing why the second rule follows, or a counterexample showing precisely how it can fail. Then a separate proof-checking system must verify that evidence.
The mathematical machines here are called magmas: sets equipped with a binary operation. The operation need not be familiar or well-behaved. Rózsa assumes neither that switching the inputs leaves the output unchanged nor that grouping operations in different ways gives the same result. Without those shortcuts, even a short-looking equation can hide a complicated search.
To say one equation implies another is to make a sweeping claim. The starting rule must hold for every assignment of its variables, and the target rule must then hold for every assignment as well. A counterexample has an asymmetry: its operation must obey the starting rule everywhere, but the search needs only one assignment that breaks the target. A proof and a counterexample are different kinds of clues, and either can be hard to find.
Consider a simple case from the paper. Suppose the starting rule says that combining an object with itself returns that object. Does this force the operation to be commutative—that is, to give the same result when two inputs are swapped? No. On a two-object set, define the operation to return its first input every time. The starting rule holds, but combining the first object with the second gives a different result from combining them in reverse order. The tiny machine is a complete counterexample.
That example hints at Rózsa’s first strategy: search for a model small enough to inspect. A finite operation can be written as a table, and the program checks whether every assignment satisfies the hypothesis while looking for a target violation. It exhaustively checks all sixteen two-element operation tables and all 19,683 three-element tables. When those avenues are too narrow, it tries larger tables, operations described by formulas, and tables that it modifies to repair violations.
But a missing counterexample proves nothing by itself. Perhaps the target really does follow. So Rózsa also searches for a derivation. It treats expressions as trees and looks for paths between the two sides of the target, applying the starting rule at different positions. A promising route can involve a detour: apply the rule to a whole expression, then apply it again inside that expression. Comparing the two results may reveal a new rule that was not obvious at the start.
In a teaching example in the paper, that overlap produces an intermediate law. A second overlap turns it into a projection rule: the operation always returns its left input. Once that rule is in hand, the more complicated target collapses through repeated applications. The useful clue was not a direct match to the goal, but two different ways to simplify the same expression. Rózsa records those steps so the eventual proof can be checked.
This is where the search gets an independent referee. Rózsa converts its proposed reasoning into a certificate for Lean, a formal proof-checking system. A proof certificate records the equalities and substitutions used; a counterexample certificate specifies the set, operation, and assignment that breaks the target. Lean checks the resulting claim. The search process may be heuristic, but an accepted certificate must pass the checker.
The solver does not bet everything on one clue. It alternates between proof searches and counterexample searches, starting with inexpensive methods and moving toward more elaborate ones. Some searches are deliberately bounded: they limit how many expressions to explore or how large a table to try. Those limits make the hunt manageable, but they also mean a true implication’s proof can exist beyond the routes Rózsa checked.
On the official 200-problem evaluation, the solver produced accepted answers for 199 cases, tying for sixth place. In a local replay, every certificate it submitted was accepted; one case remained unsolved. That distinction matters. The program did not offer a wrong proof for the missing case. It found no certificate. Its later analysis also ruled out one attempted intermediate projection law, but did not settle whether the original implication was true or false.
A second test exposed a deeper trap. Researchers selected 200 true implications that were separated by known paths of 15 to 19 steps in a graph of established results. Rózsa solved 197 without simply following those paths. But on a different set of 821 boundary cases, it solved only 147. For 819 of those cases, no finite magma can serve as a counterexample: if the implication fails, the separating structure must be infinite. Rózsa’s successful answers there all came from one special infinite construction or its reverse, and all 147 successes involved just six starting rules.
That is the puzzle’s unresolved edge. A finite table can expose a false claim, and a derivation can establish a true one. But a search that finds neither has not discovered a third answer called “probably.” It has only reached the edge of its methods. Rózsa’s results show how powerful it can be to search both sides of a mathematical question—and how important it is to keep the verdict separate from the limits of the search.
