Papers With

← All papers
First page of Ramanujan-type congruences for the smallest parts function

Ramanujan-type congruences for the smallest parts function

Larry Rolen

math.NT Nov 3, 2026 · v1
formalization autoformalization number-theory
Read PDF arXiv abstract Code
TL;DR
The paper's classification of Ramanujan-type congruences for spt(n) was autoformalized and verified in Lean by AxiomProver, with files in a public repository.
Abstract
In a famous paper of Andrews, he defined and studied the smallest parts function $\operatorname{spt}(n)$. He showed that it satisfies the three Ramanujan-type congruences: \[ \operatorname{spt}(5n+4)\equiv0\pmod5,\qquad \operatorname{spt}(7n+5)\equiv0\pmod7,\qquad \operatorname{spt}(13n+6)\equiv0\pmod{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 $\operatorname{spt}$, showing that if $\operatorname{spt}(\ell n+b)\equiv0\pmod\ell$ for all $n\geq0$, where $\ell\geq5$ is prime, then $(\ell,b)\in\{(5,4),(7,5),(13,6)\}.$ That is, Andrews' congruences are the only Ramanujan-type congruences for $\operatorname{spt}(n)$. These results have been verified in Lean by AxiomProver.
Problem

Andrews proved three Ramanujan-type congruences for the smallest parts function spt(n), modulo 5, 7 and 13. Prior work showed these are the only canonical congruences (24b ≡ 1 mod ℓ). The open question was whether any non-canonical congruences spt(ℓn+b) ≡ 0 mod ℓ exist.

Approach

Any non-canonical congruence is first shown to propagate to a whole quadratic-character class, using a quadratic twist of the mock modular generating function. Constant terms of products of half-integral weight weakly holomorphic forms then relate their coefficients. Lifting these forms to X_0(6) through Borcherds products and Shimura lifts gives a differential congruence, which supersingular points obstruct. Large primes are handled with Treviño's character-sum bound, and smaller primes are excluded directly. The proofs were autoformalized and verified in Lean by AxiomProver.

Results

For a prime ℓ ≥ 5, spt(ℓn+b) ≡ 0 mod ℓ for all n forces 24b ≡ 1 mod ℓ. Hence (ℓ,b) ∈ {(5,4),(7,5),(13,6)}: Andrews' congruences are the only Ramanujan-type congruences for spt. The Lean verification files are posted at github.com/larryrolen/SPT_noncanonical.