# A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver

arXiv: https://arxiv.org/abs/2609.00706 · HTML: https://mlsanity.com/paper/2609.00706/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 14 references that are in the map.
- First posted on arXiv 1 Sep 2026.

## Builds on (most cited first, 3 of 3)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale](https://mlsanity.com/paper/2512.07087/) (2025)
- [Distilling Many-Shot In-Context Learning into a Cheat Sheet](https://mlsanity.com/paper/2509.20820/) (2025)

## Abstract (arXiv)

The SAIR Mathematics Distillation Challenge on Equational Theories asks a solver to classify whether one magma identity implies another and, for either verdict, to return a certificate accepted by a deterministic Lean judge. We present a single-file solver organized as a cheapest-first cascade. Its false branch combines coefficient tests over structured algebra families, bounded finite-model search, an explicit central-groupoid witness, and several infinite-carrier witnesses. Its true branch is a proof-producing ordered unit superposition procedure with Knuth-Bendix ordering, bidirectional demodulation, indexing, memoised substitution, and anytime size deepening. Search results remain outside the trusted base: successful derivations are replayed as small Lean terms, and countermodels are rechecked by the competition judge. The frozen solver is a 189,504-byte Python file with SHA-256 f2392533c9f4c03b.... In local runs through official judge revision 2848228, it produced accepted certificates for all 1,889 rows of the six public sets with no language-model calls. Separate measurements recorded full agreement on the 800 published Stage 1 evaluation-distribution problems, 100 accepted rows in the canonical Marathon manifest without tokens, and 200 accepted rows in the hosted playground. These are regression and playground measurements, not a leaderboard result and not evidence about a hidden set. All quantitative claims are tied to immutable result ledgers; the paper makes no completeness or comparative-superiority claim.