Imagine being handed two rules for an unfamiliar kind of arithmetic. The first is a starting assumption; the second is a claim you want to test. Does the first rule force the second to be true? There may be no familiar shortcuts. The operation need not behave like addition or multiplication: it is not assumed to be associative, commutative, or anything else. Even the parentheses matter.
That is the challenge Georgios Kissas’s program Rózsa takes on. Instead of betting everything on one style of proof, it attacks the question from both sides. If the claim follows from the assumption, it tries to build a derivation. If it does not, it tries to construct a mathematical world where the assumption holds but the claim breaks. Either way, it must produce evidence that a separate proof-checking system, Lean, can verify.
The key is a shift in perspective: the program does not need to guess the answer first. It can search for the kind of object that would settle the question. A proof is one such object. A counterexample is another. Both searches are fallible and bounded; the certificate, not the search strategy, is what makes an accepted answer trustworthy.
First, preserve every detail. Rózsa stores each expression as a branching tree. Variables sit at the leaves, and each use of the binary operation joins two branches. That distinction matters because the program cannot silently rearrange parentheses. In ordinary arithmetic, people often treat different groupings as equivalent. Here, doing so could change the problem itself.
Then the program tries relatively direct routes. It checks whether the target can be reached by repeatedly applying the assumed rule to pieces of an expression. Each move is logged. If a useful path appears, the record becomes a proof: apply the assumption, replace an equal piece inside a larger expression, and connect the resulting steps.
But some consequences are not visible in a straight line. So Rózsa also looks for overlaps: places where two differently positioned copies of the assumed rule can apply to the same expression. The two routes may lead to different results, and the equality between those results becomes a new rule to investigate. That rule may unlock another one, and eventually help reach the original target. The method is a little like finding a hidden passage by examining where two corridors cross—but every step is written down, not merely intuited.
The other route searches for a world in which the target fails. A binary operation on a small set can be written as a table: for every pair of inputs, the table names an output. Rózsa checks small tables, but also tries more structured possibilities, including operations defined by simple formulas. Instead of inspecting every possible table, it can search over the compact recipe that generates one. For some cases it uses a constraint-solving method to fill in an unknown table while enforcing the assumed rule and demanding at least one target violation.
Finding a single failed instance of the target is not enough. The program must also show that the assumed rule holds for every possible assignment in its proposed world. That distinction is crucial: a counterexample has to refute the implication, not merely produce a suspicious-looking calculation. For finite worlds, the certificate can check the whole operation. The paper also describes a fixed infinite construction, where a proof must establish the starting rule across the entire infinite set—not just sample a few elements.
Once either search finds evidence, Rózsa turns its record into Lean code. For a proof, that means reconstructing the chain of equalities and the rule behind each move. For a counterexample, it means defining the world and operation, proving the hypothesis holds there, and identifying an assignment where the target fails. Lean then checks the submitted certificate independently. If the search makes a mistake, a plausible-looking answer is not enough to pass.
On the challenge’s 200-problem main evaluation, the submitted solver solved 199 cases, or 99.5 percent, and was tied for sixth place. In the author’s local rerun, the mathematical search methods—without the optional language-model fallback—also solved the same 199 cases. Every certificate submitted in that rerun was accepted. The one remaining case was unsolved: that does not mean the implication was false, only that the bounded search did not find a certificate.
To probe beyond the main benchmark, Kissas tested Rózsa on selected implications whose known proofs could be traced through chains of 15 to 19 earlier results. The program solved 197 of 200 without simply following those known chains. But a different test exposed a sharper boundary. Among 821 selected cases that require an infinite counterexample, it solved 147. All those successes came from the same fixed infinite construction or its reversed operation. The paper is explicit that this is a narrow tool, not a general way to discover infinite worlds.
That unevenness is part of the story. Rózsa can be impressively effective when proof search, small models, or its special infinite construction fit the problem. It can also run out of search options even when more time remains, because its strategy uses preset limits rather than endlessly widening its hunt. A failure to solve a case is not a mathematical verdict.
The broader idea is more modest—and more useful—than a machine that simply announces truths. Treat mathematical reasoning as a hunt for checkable evidence, and let different searches bring different clues: a rewrite, an overlap, a filled-in table, a carefully defined infinite structure. The searcher may be clever, incomplete, or wrong about where to look. But when it succeeds, the proof checker can inspect the trail. In a field where a one-character change in parentheses can alter the question, that separation between finding an answer and verifying it is a powerful new approach.
