Algebraic geometric framework of Rogers–Ramanujan identities
Yifeng Huang, Kenny Lau, Ken Ono, Peter Paule
math.NT
Aug 15, 2026 · v1
math.CO math.RT
TL;DR
The Rogers–Ramanujan-type identities proved for the (3,b) cases were formalized and verified in Lean by AxiomProver.
Abstract
The Rogers–Ramanujan identities equate a $q$-series whose exponents are governed by a quadratic form with an infinite product supported on two residue classes modulo $5$. Identities of this shape are scarce, and a central problem is to identify the structures that produce them in families. Huang, Jiang, and Oblomkov have proposed a source of a new kind: to each pair of coprime integers $a,b>1$ they attach an infinite-rank $q$-series $Z_{a,b}(q)$, assembled from counts of commuting nilpotent matrix pairs $(A,B)$ with $A^a=B^b$ over finite fields, and they conjecture that it equals an explicit product of $(a-1)(b-1)/2$ modular units of level $a+b$. The $a=2$ cases are the Andrews–Gordon identities; no case with $a>2$ was known. We prove the conjecture for $(a,b)=(3,4)$, $(3,5)$, $(3,7)$, and $(3,8)$. Our proofs pass through a finer sum-to-sum identity, which we conjecture for all $b$ coprime to $3$ and establish for all $b$ when $q=1$. Lau and Ono have since proved that identity in general, and with it the full $a=3$ case. These identities have been formalized and verified in Lean by AxiomProver.
Problem
Rogers–Ramanujan identities equate quadratic-form q-series with modular product forms; such families are rare. Huang, Jiang, and Oblomkov conjectured that q-series Z_{a,b}(q) built from commuting nilpotent matrix pairs equal explicit products of modular units, with no case a>2 previously known.
Approach
A finer sum-to-sum identity is conjectured for all b coprime to 3 and established at q=1 combinatorially. Specific cases (a,b)=(3,4),(3,5),(3,7) are proved via the q-Vandermonde identity, and (3,8) via a computer-assisted annihilator method. The resulting identities were formalized and verified in Lean by AxiomProver.
Results
The conjecture is proved for (3,4), (3,5), (3,7), and (3,8), and the q=1 specialization is established for all b. These identities were formally verified in Lean.