Class polynomial obstructions to canonical congruences for the smallest parts function
Larry Rolen
math.NT
Oct 19, 2026 · v1
TL;DR
The paper's proofs were formally verified in Lean by AxiomProver, with the formalization files posted in a public GitHub repository.
Abstract
We resolve an open conjecture by proving that the only "canonical” Ramanujan congruence primes for the Andrews' smallest parts function, $\operatorname{spt}(n)$, are $\ell= 5, 7, 13$. Building on work of Ahlgren and Kim, we show that any such congruence forces square-index coefficients of certain weakly holomorphic forms of weight $1/2$ to vanish modulo the congruence prime. A normalized Borcherds product converts this into the vanishing of the derivative of a quotient of two oriented CM polynomials on $X_0(6)$. A quaternionic volume estimate in an Eichler order of level $6$ prevents that vanishing when a suitable inert discriminant is small. Treviño's character estimate supplies such a discriminant for every prime at least $10^{11}$. The remaining range is covered by the previous calculations of Ahlgren and Kim. These results have been verified in Lean by AxiomProver.
Problem
Andrews proved Ramanujan-type congruences for the smallest parts function spt(n) modulo 5, 7 and 13. It was a long-standing conjecture that these are the only 'canonical' congruence primes.
Approach
Building on Ahlgren and Kim, a canonical congruence is shown to force square-index coefficients of certain weight 1/2 weakly holomorphic forms to vanish modulo ℓ. A normalized Borcherds product turns this into the vanishing of the derivative of a quotient of oriented CM class polynomials on X_0(6). A quaternionic volume estimate in an Eichler order of level 6 rules out that vanishing when a small inert discriminant exists. Treviño's character bound supplies such a discriminant for all primes ℓ ≥ 10^11. The proofs were then verified in Lean by AxiomProver.
Results
The canonical congruence primes for spt(n) are exactly 5, 7 and 13. Primes below 10^11 are covered by the earlier computations of Ahlgren and Kim, and the arguments were formally verified in Lean.
