A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver
Haobo Ma, Wenlin Zhang, Manuel Israel Cázares
cs.CL
Quick verdict
Lean-verified cascade accepts all 1,889 public EQT2 rows with zero LLM calls; honest claims, though tuned on public residuals with no external baseline.
Summary
This paper presents a single-file Python solver for Stage 2 of the SAIR Mathematics Distillation Challenge on Equational Theories, which asks whether one magma identity implies another and requires, for either verdict, a certificate accepted by a deterministic Lean 4 judge. The solver runs a cheapest-first cascade: the false branch combines coefficient tests over structured algebra families, bounded finite-model search over carriers 4–10 with Latin-square propagation, one hardcoded order-9 central groupoid, and infinite-carrier Austin witnesses; the true branch is a proof-producing ordered unit superposition engine with Knuth–Bendix ordering, bidirectional demodulation, and anytime deepening. Search stays outside the trusted base: derivations replay as small Lean terms and countermodels are rechecked by the judge. Against official judge revision 2848228, the frozen solver accepted all 1,889 six-public-set rows, all 800 Stage 1 distribution problems, 100 Marathon rows, and 200 stress-test problems with zero language-model calls, while certifying 0 of 100 research_order5_hard problems. The paper candidly discloses two implementation failures and asserts no completeness, hidden-set, or superiority claim. Main limitations: components tuned on public residuals, several measurements being operator attestations without hash-bound ledgers, single-host timings, and no external prover baseline.
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 2
● low 2
5 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- The frozen v2.5 solver produced judge-accepted certificates for all 1,889 rows of the six public sets, all 800 Stage 1 distribution problems, 100 Marathon rows, and 200 stress-test problems, with zero language-model calls (Tables 1–2, §8.4).
- Only the Lean 4 kernel, dependency inspector, and judge are trusted; solver defects can cost time or coverage but cannot produce an invalid acceptance (§2.1).
- Two implementation failures — tautology retention in the active set and inconsistent asterisk/diamond input normalization — were consequential and were exposed by end-to-end certificate runs rather than label accuracy (§4.2, §5.2).
- The solver certifies 0/100 research_order5_hard problems, delimiting finite methods against order-five Austin laws whose false direction admits no finite countermodel (§8.4).
- The paper makes no completeness, hidden-set, leaderboard, or comparative-superiority claim (Abstract, §8.1).
Strengths
Kernel-only trust boundary
§2.1: verdicts require polarity-correct candidates checked by the official Lean judge and dependency inspector; search defects 'cannot cause an invalid certificate to be accepted'. Every accepted row in Table 1 had exactly one judge call.
Hash-bound provenance discipline
§8.3: PROVENANCE.json binds solver SHA-256 (189,504 bytes), judge revision 2848228, and every ledger; scripts/check_freeze.py 'fails closed on drift'; a full revalidation under the upgraded Lean 4.33.1 judge is committed (results/lean4331_revalidation/).
Honest, tightly delimited claims
Instructive failure analyses
Broad, fully accepted measurable coverage
Weaknesses
Residual-driven design without controlled ablation
No external prover baseline
Several headline numbers are attestations, not ledger-bound evidence
Single-host timing without variance
Artifact availability left unstated
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
This is a systems paper describing solver v2.5 for Stage 2 of the SAIR Mathematics Distillation Challenge on Equational Theories: given two magma identities E1, E2, decide whether E1 implies E2 and emit a certificate — a Lean 4 proof of the universal implication for 'true', or an existential countermodel for 'false' — accepted by the deterministic official judge (§1, §2.1). The authors claim exactly three things: (1) a single-file, hash-bound cascade (189,504 bytes, SHA-256 f2392533c9f4...) whose outputs cover all 1,889 rows of the six public sets (Table 1), all 800 published Stage 1 evaluation-distribution problems, 100 Marathon manifest rows, and 200 stress-test rows, with zero language-model calls; (2) a trust boundary in which only the Lean kernel and dependency inspector are trusted (§2.1); and (3) an explicit refusal of completeness, hidden-set, or comparative claims (§8.1). A fourth, valuable negative datum: 0/100 acceptances on research_order5_hard (§8.4).
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What does this paper's solver do?
It solves Stage 2 problems of the SAIR Equational Theories challenge: given two identities of a magma (a set with one binary operation and no assumed laws), it decides whether the first implies the second and outputs a machine-checked Lean 4 certificate — a proof of the implication if true, or a concrete counterexample magma if false.
Did the solver use a large language model?
No. All 1,889 accepted public-set rows came from the deterministic cascade with zero language-model calls. A controlled test of the organizer-pinned gpt-oss-120b fallback solved 0 of 6 residual problems, at a measured cost of $0.1350.
Did it win the competition?
No leaderboard result exists in this paper. The measurements are local regressions through the official Lean judge (revision 2848228), a distribution drill, a Marathon batch run, and a hosted playground attestation; the hosted score is explicitly listed as PENDING, and no hidden-set performance is claimed.
Can I reproduce the results?
The paper gives exact replay commands (§8.4): verify hashes with scripts/check_freeze.py, then run the official runner at pinned judge revision 2848228 with the frozen solver, plus a Marathon script for the batch manifest. This requires the authors' artifact repository, for which the text states no public URL.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- The metadata abstract is cut mid-sentence ('no com'), but the complete abstract sentence appears in the extracted body text; nothing in the paper text itself is genuinely truncated.
- PROVENANCE.json, the result ledgers, and the solver source are referenced but not embedded in the PDF text, so hash bindings and per-row results cannot be independently verified from the paper alone.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.