Search papers, labs, and topics across Lattice.
This paper introduces a novel solver for the SAIR Mathematics Distillation Challenge that efficiently classifies equational implications between magma identities while producing verifiable certificates for a deterministic Lean judge. The solver employs a cheapest-first cascade approach, integrating techniques such as coefficient tests, bounded finite-model search, and a proof-producing ordered unit superposition procedure. Remarkably, it achieved accepted certificates for all 1,889 test cases without invoking language models, demonstrating both robustness and efficiency in handling complex algebraic structures.
Achieving 100% success in certifying equational implications without relying on language models showcases a breakthrough in automated theorem proving efficiency.
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.
