Tagewerk IV
Kernel-verification of a COLT-2021 open-problem refutation (SS–RS–GD), with a caught erratum
Yun–Sra–Jadbabaie (COLT 2021) asked whether single-shuffle SGD can beat reshuffle SGD and GD in the well-conditioned regime (Conjecture 1.1). A pipeline-math write-up refutes the SS–RS half at (n,K)=(3,2). We kernel-verified the refutation's algebraic core against Lean 4.31: the gap identity (1.8), the positivity of its final factor, the violation λ_SS > λ_RS on the interval, and a fully concrete witness at q=1/2 — every headline theorem with only the standard axioms. Conjecture 1.1 is machine-refuted. Two by-products of routing it through the kernel: an LLM scout's claim that a sum-of-squares identity was wrong was itself refuted (the paper is correct — the scout dropped a cross-term); and the paper's supporting identity (1.7) was found NOT to hold as printed (Lean ring plus an independent exact-rational check agree), a supporting-lemma erratum that does not affect the main result (the inequality λ_RS ≥ μ_RS it targets still holds). The erratum was reported upstream.
Verdicts — machine-adjudicated (3)
- VERIFIED R1 The refutation core (gap identity + violation + concrete witness)
gap_identity (λ_SS − λ_RS = (1−q)⁶(q+1)² g(q)/2048), gg_pos, ss_exceeds_rs on [1/4,1), and violation_at_half all kernel-decided; #print axioms = standard set. Conjecture 1.1 is false.
- CORRECTED R2 An LLM scout's flagged 'error' in a sum-of-squares identity
The scout claimed q⁴−8q³+30q²−8q+1 = (q²−4q+1)²+12q² was off by 2q²; the kernel confirms the paper is right — (q²−4q+1)² = q⁴−8q³+18q²−8q+1, so +12q² gives 30q². LLMs propose; the kernel decides.
- ERRATUM R3 Paper's supporting dominance identity (1.7)
As printed, λ_RS − μ_RS does not equal the displayed right-hand side (leading-coefficient mismatch: 16q¹²/16384 vs 15q¹²/16384). Confirmed by Lean ring and independent exact-rational arithmetic. Supporting-lemma only; the intended inequality still holds and the refutation (via 1.8) is unaffected. Reported upstream.
Re-runnable artifacts
- ss_rs_gd_refutation.lean ↓ sha256 aa4c1ca907d2…
Files download verbatim from this site — the exact kernel-checked bytes (verify the SHA-256). See how to re-verify.
Repositories — the code trail
- audited Pengbinghui/pipeline-math @ 69d7df7 papers/ss-rs-gd.pdf (the refutation write-up)
- produced elementalcollision/leibniz-daemon #274 scripts/ss_rs_gd_lean.py + docs/colt/ss_rs_gd_refutation.lean
- contributed Pengbinghui/pipeline-math #4 erratum report on the supporting identity (1.7)
References
- Yun, C., Sra, S., & Jadbabaie, A. (2021). Open problem: Can single-shuffle SGD be better than reshuffling SGD and GD? In Proceedings of the 34th Conference on Learning Theory (Vol. 134, pp. 4653–4658). PMLR.
- Peng, B., Tao, R., Wang, S., Yu, H., & Liu, D. (2026). pipeline-math [Computer software]. GitHub. https://github.com/Pengbinghui/pipeline-math
- Recht, B., & Ré, C. (2012). Toward a noncommutative arithmetic-geometric mean inequality: Conjectures, case-studies, and consequences. In Proceedings of the 25th Annual Conference on Learning Theory (Vol. 23, pp. 11.1–11.24). PMLR.