Tagewerk IV
Kernel-verification of a COLT-2021 open-problem refutation (SS–RS–GD), with a retracted 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. A by-product 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). Correction, 2026-10-13: this cycle first reported that the paper's supporting identity (1.7) does not hold as printed, and we filed that as an erratum upstream. The error was ours. Our transcription of μ_RS dropped the square the paper prints on its quartic factor; with μ_RS as printed, (1.7) holds and is now kernel-verified. The kernel decided correctly on the statement we gave it; the statement was wrong. The upstream report was retracted the same day.
Verdicts — machine-adjudicated (4)
- 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.
- VERIFIED R3 Paper's supporting dominance identity (1.7)
Corrected 2026-10-13. With μ_RS as printed, (q+1)⁴(q⁴+4q³−42q²+4q+1)²/16384, λ_RS − μ_RS equals the displayed right-hand side identically (dominance_mu_1_7, Lean ring; standard axioms). This finding first read ERRATUM; see R4.
- RETRACTED R4 Our 2026-07-04 erratum report on (1.7)
Our transcription of μ_RS dropped the square on its quartic factor, which made (1.7) look false (leading coefficient 16q¹²/16384 against 15q¹²/16384). Lean ring and our exact-rational check both agreed, because both were given the same wrong formula. The mis-transcribed statement is kept in the corrected certificate as a labelled negative control (mistranscribed_1_7_false_at_half). Retracted upstream on 2026-10-13.
Re-runnable artifacts
- ss_rs_gd_refutation.lean ↓ sha256 9642f206663e…
- ss_rs_gd_refutation.retracted-2026-07-04.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); retracted 2026-10-13 (our transcription error)
- produced elementalcollision/leibniz-daemon #424 the correction: muRS with the paper's square, dominance_mu_1_7, and the negative control
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.