Source-linked AI summary
A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver
Haobo Ma, Wenlin Zhang, Manuel Israel Cázares
TL;DR
The paper addresses certificate-producing classification of whether one magma identity implies another under a deterministic Lean judge. It presents a cheapest-first cascade combining structured and irregular countermodels with proof-producing superposition, then replays or rechecks candidates in Lean. The frozen solver accepted all 1,889 rows of six public sets in local regression, while the paper explicitly withholds completeness, hidden-set, leaderboard, and comparative claims.
Problem
Equational implication requires both a verdict and a certificate accepted by a deterministic Lean judge, rather than classification alone.
Method
A single-file cheapest-first cascade combines coefficient-based and finite or infinite countermodels with ordered unit superposition, while Lean replays proofs and rechecks countermodels.
Results
1,889 rows were accepted across the six public sets in local regression, while focused prover measurements found all 254 development derivations and all 819 public true proofs under their stated caps.
Takeaways & Limitations
The system provides an auditable certificate-production and regression framework whose accepted outputs are determined by judge checking rather than untrusted search results.
Takeaways & Limitations
The measurements are development and published-data regressions under specific environments, not evidence of completeness, hidden-set performance, leaderboard standing, or comparative superiority.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper frames equational implication as a certificate-production problem: solvers must classify magma identities and emit Lean-checkable proofs or counterexamples. It presents a deterministic cascade whose search remains untrusted while accepted outputs are validated by the official judge.
- Problem: The task asks whether one magma identity implies another, requiring a Lean 4 proof for true answers or a separating magma for false answers.Magma operations assume no associativity, identity, or cancellation law.
- Certificate contract: Certificate production changes the objective from classification alone to reconstructing a kernel-checkable witness.Search defects can prevent solutions but cannot make the judge accept an invalid certificate.
- Architecture: The solver uses a deterministic-first cascade combining inexpensive countermodel families, bounded finite-model search, and proof-producing superposition.The same single-file source supports Solo and Marathon execution protocols.
- Scope: The reported scope is a system description and auditable regression report, not a completeness theorem about single-identity implications.The countermodel families and superposition implementation are not proved complete, and deeper stages have wall-clock limits.
- Contributions: The paper reports four contributions spanning integrated countermodel and proof branches, judge-compliant certificate encodings, failure analysis, and hash-bound provenance.End-to-end certificate runs exposed tautology-retention and operator-spelling failures.
2 Single-File Solver Architecture
The solver is a single-file, cheapest-first cascade whose stages independently produce and validate polarity-correct certificates. Its trusted boundary is the Lean judge, while scheduling, parsing, replay, and batch execution manage search under fixed budgets.
- Trusted interface: The judge accepts only a type-correct certificate matching the generated true or false goal and satisfying dependency inspection.Search remains an untrusted producer; Lean elaboration, kernel checking, and policy inspection determine acceptance.
- Trusted interface: Each stage returns a self-contained candidate and continues after rejection, preventing unverified search outcomes from determining the verdict.Failed countermodels and unreplayable proof traces are discarded rather than cached as Boolean evidence.
- Cascade stages: The cascade progresses from shallow structured countermodels and direct proofs to bounded irregular models, deep false search, and anytime superposition.Recorded budgets include eight seconds for bounded finite-model search, up to 120 seconds for a later finite-model pass, and up to 600 seconds for deepest proof search.
- Cascade stages: Positive recognizers dispatch stages from parsed equations and require concrete substitutions, equality chains, or separating evaluations before emission.Equation identifiers support diagnostics only; matching parsed laws supports replay across variable-order and labeling differences.
- Execution modes: Marathon mode uses stable structural-cost triage, two-pass scheduling, durable JSONL output, and no speculative language-model calls.The batch path retains verified deterministic answers and may leave residual rows unanswered when budgets expire.
4 Proof-Producing Ordered Superposition
The true branch uses ordered unit superposition to search for equational implications, then replays successful derivations as positive Lean 4 equality chains. Its budget-bounded implementation combines demodulation, indexing, memoisation, adaptive caps, and explicit safeguards against search failures.
- Architecture: The engine specializes ordered superposition to one binary symbol, unit clauses, and replayable positive Lean 4 proofs.It derives the goal identity rather than emitting only a refutation result.
- Inference: Knuth–Bendix ordering orients usable equations, while superposition overlaps maximal sides at non-variable positions after unification.Ordering checks are repeated after substitution because unification can change comparisons.
- Search control: Bidirectional demodulation, alpha-normalized keys, weighted-and-aged given-clause selection, and cached term data organize saturation.The implementation interleaves weight and age priorities and varies them across deepening rounds.
- Failure analysis: Deleting demodulated tautologies fixed a public residual that previously remained unsolved after 810 seconds.Retained tautologies attracted selection and displaced clauses on the useful derivation.
- Failure analysis: The corrected prover found that residual in 0.6 seconds directly and produced an accepted certificate in 14.6 seconds under the official runner.These measurements illustrate coupling between simplification and selection, not a general speed ratio.
- Scope: The procedure is budget-bounded and machine-load sensitive, without a completeness result for ordered superposition or fairness under every cap.Evaluation measures this implementation on fixed corpora.
- Certificate replay: Replay reconstructs only reachable derivation recipes as named equality steps using instantiation, congruence, symmetry, and transitivity.Search remains outside the Lean kernel, which checks the emitted term and rejects incorrect reconstruction.
5 Engineering for the Hosted Environment
The solver was engineered for a constrained hosted environment with protocol-sensitive input handling, bounded resources, and toolchain variation. Encoding normalization and certificate re-emission addressed failures that otherwise prevented or delayed accepted results.
- Toolchain compatibility: The public harness used Lean 4 4.30.0-rc2, while the hosted verifier used Lean 4 4.32.0 with corresponding Mathlib.An Austin certificate initially required about 330 seconds to compile under the larger environment.
- Toolchain compatibility: Rewriting the Austin certificate with explicit core lemmas reduced its Lean 4 4.32 compilation to 3.1 seconds.The compatibility corpus compiled 119 of 120 accepted certificates under the exact announced toolchain.
- Input encoding: A parser that normalized only one operation spelling crashed before search and recorded zero accepted rows out of 800.The official judge normalized asterisk and diamond spellings, but the runner passed original problem text to the process.
- Input encoding: After normalization at both Solo and Marathon intakes, the same drill recorded 800 accepted certificates with full agreement against published answers.Normalization must occur before dispatch or caching.
- Resource constraints: The sandbox’s read-only mount, bounded processes and memory, absent network, and small temporary filesystem force a standard-library, single-file design.Bounded queues and caches keep long false saturations below the observed memory ceiling.
- Resource constraints: Marathon requires flushed, synchronized output because its output file is the only durable mutable state supplied by the runner.Redirecting judge artifacts to temporary storage resolved an unwritable default artifact directory without changing judge sources.
6 End-to-End Certificate Production
End-to-end certificate production validates candidate countermodels and proof derivations before submission, while Lean and the official judge remain responsible for final acceptance. The transaction supports finite, structured, and infinite witnesses as well as Solo and Marathon execution.
- Finite countermodels: Finite countermodel candidates are checked for carrier validity, hypothesis satisfaction on every required assignment, and goal separation before Lean emission.Any failed check discards the candidate witness.
- Finite countermodels: Small finite witnesses use a table-based magma and finite decision to expand the universal hypothesis and existential counterexample.The stored Python assignment prechecks the candidate, but the accepted theorem does not rely on the Python evaluator.
- Structured carriers: Larger structured carriers define the operation with transparent Nat and Fin primitives, keeping multi-digit entries outside the direct table helper.Packed tables use natural-number payloads and indexing expressions, while arithmetic families print closed forms.
- Validation: Certificate validation has independent model and dependency failure modes, so development probes must use the complete official policy.A permissive harness once made a rejected arithmetic shape appear usable.
- Infinite witnesses: Infinite Austin witnesses match the hypothesis to a stored law, instantiate an operation on N, and find a concrete tuple separating the goal sides.The emitted witness packages the carrier, magma instance, hypothesis theorem, and contradiction from an assumed goal equality.
- True certificates: Superposition replay orders only the inference recipes reachable from a refutation and reconstructs overlaps with congrArg, symmetry, and transitivity.The resulting Lean source contains only the equational consequences needed for the final chain.
- Execution modes: Solo submits complete sources directly, whereas Marathon durably appends candidate rows for post-exit verification using the same proof policy.The difference changes scheduling and commit timing, not trust.
7 Evaluation
The evaluation reports accepted certificates across public, distribution-drill, Marathon, and hosted-playground measurements, while carefully limiting what these results establish. Results are tied to specific runners, budgets, ledgers, and measurement settings rather than presented as hidden-set or completeness evidence.
- Six public sets: 1,889 rows across six public sets were accepted, each with one judge call and no fallback-model use.The earlier v1 solver accepted 1,875 rows, reported only as development context rather than an entrant comparison.
- Scope and interpretation: The evaluation is a regression and readiness report, not evidence of completeness, hidden-set performance, or aggregate component gains.Several changes were introduced together, and the paper attributes mechanisms only where direct replay evidence exists.
- Distribution drill: Four published Stage 1 evaluation-distribution splits achieved full local judge acceptance and full agreement with published labels.Because Stage 2 did not reuse these problems, the drill measures format and distribution readiness rather than evaluation transfer.
- Marathon and hosted playground: The canonical Marathon manifest accepted all rows without tokens, while the hosted playground accepted every attempted problem with no rejected or errored rows or language-model calls.The hosted result is an operator attestation, not an official leaderboard score.
- Hosted timing: The hosted playground recorded mean times of 2.69 seconds for false rows and 7.08 seconds for true rows, with maxima of 6.5 and 23.8 seconds.These values include hosted orchestration and certificate checking and are not directly comparable to the local prover-only benchmark.
- Focused prover measurement: The focused G3 measurement found all 254 difficult derivations and all 819 public true problems under stated caps, but these prover-only results lack standalone hash-bound runner ledgers.The measurements are not judge wall-clock results and do not claim superiority over Vampire.
8 Honest Boundary and Reproducibility
The paper reports an explicit empirical boundary: archived certificates cover measured corpora, but no hidden-set transfer, completeness, leaderboard, or comparative-superiority claim follows. Reproduction is tied to pinned artifacts, commands, hashes, and judge environments, with compatibility and portability limitations.
- Honest boundary: There is no hosted leaderboard score or rank, and the reported local and playground measurements do not establish transfer to the hidden evaluation distribution.The hosted playground is diagnostic, while six-set and distribution-drill results are local official-runner measurements.
- Honest boundary: The solver has no completeness theorem: countermodels cover selected families, finite search is bounded, and superposition stops at deadlines.Deepstage outcomes can vary with machine load, and the paper makes no performance-superiority claim over another solver or prover.
- Threats to validity: The distribution drill is published Stage 1 data whose construction patterns and ground truth may overlap with the public suites, limiting its independence.The authors describe full regression as evidence of integration rather than performance on an independently sampled corpus.
- Threats to validity: Wall-clock totals reflect one operator-host environment, with timing affected by worker load and filesystem caching rather than portable runtime behavior.Hosted-playground means partially address the environment gap but use a different protocol from final evaluation.
- Reproduction: Reproduction uses pinned checkouts, freeze verification, official runner commands, and new output hashes rather than overwriting archived ledgers.The provenance record binds solver, configuration, result-ledger, Marathon, compatibility, and playground artifacts.
- Reproduction: The Lean 4 4.32 compatibility corpus is externally described but not packaged as a one-command repository test, and hosted interaction requires organizer infrastructure.The official harness, freeze checker, ledger files, and public-runner commands remain locally available.
- Measured outer boundary: On stage2_stress_test, the frozen solver accepted 200 of 200 problems, while on research_order5_hard it certified none within budget.The paired ledgers mark complete coverage of the announced evaluation distribution and a frontier beyond the solver’s finite methods.
9 Related Work
The paper situates its solver between formal equational-theory resources, mature superposition provers, Lean-based certificate checking, and distillation-oriented artifact design. Its distinctive focus is a specialized, certificate-producing interface rather than label prediction or unrestricted theorem proving.
- Equational theories: The Equational Theories Project supplies implication graphs, formal proofs, finite models, and curated data, while Stage 2 requires a judge-accepted proof or countermodel.The SAIR task adopts the project’s single-magma-identity setting but adds an online solver and certificate interface.
- Equational theories: The central-groupoid and Austin witnesses reuse constructions represented in prior equational-theory work without claiming a general finite-model theorem.The central-groupoid use is specifically a checked non-natural finite model for the E168 witness family.
- Superposition provers: The superposition engine borrows ordered inference, KBO, demodulation, indexing, and selection ideas from mature provers but specializes them to unit equations over one binary symbol.Its system-level distinction is the output contract, which compiles the search trace into a certificate.
- Proof assistants and certificate checking: Lean 4 serves as both certificate language and trusted checker, with untrusted automation reconstructed or checked by the kernel and finite countermodels treated as proof objects.Exhaustive reflection closes concrete finite statements, while infinite witnesses use core lemmas.
- Distillation artifacts: Unlike a natural-language distillation sheet, this artifact distills algebraic families, search control, and proof printers into executable source code.The fixed-configuration language-model measurement documents development rather than arguing that symbolic search and language models are mutually exclusive.
10 Conclusion
The paper concludes that its cheapest-first cascade meets the certificate-producing contract through complementary countermodels and proof-producing superposition replayed by Lean 4. Its evidence remains bounded by hash-bound regressions and explicitly excludes leaderboard, hidden-set, completeness, and comparative claims.
- Conclusion: The solver combines structured and irregular countermodels, infinite witnesses, and ordered unit superposition, then replays accepted results through the Lean 4 kernel.The same artifact supplies a machine-checked reason for either polarity.
- Conclusion: Hash-bound local regressions cover measured public and distribution-drill rows, while a separately labeled hosted-playground measurement exercises the announced toolchain.These measurements are presented as bounded evidence rather than broad evaluation claims.
- Conclusion: The paper reports no leaderboard result, hidden-set claim, completeness theorem, or comparative claim at this draft stage.The conclusion states the remaining boundary explicitly.
Author contributions (CRediT)
The listed contributors jointly handled conceptualization, methodology, software, investigation, and validation, with additional roles in data curation, administration, writing, and freeze verification.
- Contributions: Haobo Ma contributed conceptualization, methodology, software, investigation, and validation.His software role covered solver architecture and the systems foundation.
- Contributions: Wenlin Zhang contributed conceptualization, methodology, software, investigation, validation, data curation, project administration, and original-draft writing.
- Contributions: Manuel Israel Cázares contributed validation of solver-freeze verification and evidence-ledger auditing, plus methodology review of experimental design.