Rózsa solver efficiently proves or disproves equations on sets
Rózsa: Certified Equational Reasoning
Logic in Computer Science
Summary
The paper studies when one equation logically implies another in sets with any binary operation, without assuming common algebraic properties like associativity. The authors present Rózsa, a Python program that tries to prove or find counterexamples for such implications using finite and one infinite model. Rózsa provides computer-checked proofs or refutations suitable for formal verification in Lean and solved nearly all tested problems. The paper explains how the solver explores these questions and discusses its strengths and current limits.
What this means in practice
- •For software verification teams: Generate machine-checked proofs or counterexamples for equations in custom algebraic systems to improve code correctness guarantees.
- •For automated theorem proving developers: Use Rózsa’s approach to efficiently combine proof search and model search for verifying equation implications in abstract algebra contexts.
Authors
Georgios Kissas
Abstract
When does one equation imply another? Stage 2 of the SAIR Mathematics Distillation Challenge required teams to submit solvers to answer this question for sets equipped with a binary operation. For these sets, associativity, commutativity, or any other algebraic property was not assumed. Each answer required a proof or counterexample that could be verified by Lean. Programs also had to respect fixed resource limits. We present Rózsa, a Python solver that searches for both kinds of evidence. It begins with simple tests and considers more extensive searches when those fail. To find a proof, it applies a given equation and derives any further equations as needed, keeping a record of each step. To find a counterexample, it searches for operations on finite sets. It also tests one fixed infinite model. The given equation must hold for every assignment, while the target equation must fail for at least one. In either case, Rózsa turns the evidence into a Lean certificate. The submitted solver solved 199/200 problems (99.5%) in the official main evaluation getting the 6th overall position. Additional tests show that the solver can prove many implications linked by long chains of known results, but has limited success with infinite counterexamples. We explain the search methods, how they fit together, and what the unsolved cases reveal about their limits.