Ramanujan-type congruences for the smallest parts function

In a famous paper of Andrews, he defined and studied the smallest parts function spt(n). He showed that it satisfies the three Ramanujan-type congruences: \[ spt(5n+4)≡05, spt(7n+5)≡07, spt(13n+6)≡0{13}. \] In a recent preprint, the author showed that these are the only "canonical'' congruences. Here, we complete the classification of Ramanujan-type congruences for spt, showing that if spt( n+b)≡0 for all n≥0, where ≥5 is prime, then (,b)∈\(5,4),(7,5),(13,6)\. That is, Andrews' congruences are the only Ramanujan-type congruences for spt(n). These results have been verified in Lean by AxiomProver.