Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond
Kenny Lau, Seewoo Lee, Ken Ono
math.NT
Jul 1, 2026 · v1
math.CO math.LO
TL;DR
Formalizes q-series theory in Lean/Mathlib, verifying the Jacobi Triple Product, Bailey's Lemma, and the Rogers-Ramanujan identities.
Abstract
The theory of $q$-series and basic hypergeometric series plays a crucial role at the intersection of combinatorics, number theory, and representation theory. From the classical partition identities of Euler and Jacobi to modern developments in class field theory, vertex operator algebras, and the Monstrous Moonshine conjecture, $q$-series provide the analytic framework for a wide range of profound applications. In this paper, we discuss the formalization of this theory in the Lean proof assistant, a process that requires careful design of scalable and versatile structures to reconcile formal algebraic identities with analytic convergence properties. We address these foundational challenges by focusing on the construction of $q$-Pochhammer symbols, $q$-binomial coefficients, Bailey's Lemma and similar primitives. To demonstrate the utility of this work, we provide fully verified proofs of the Jacobi Triple Product formula and the celebrated Rogers-Ramanujan identities, which serve as both historical and technical benchmarks for the field. This work establishes a rigorous computational foundation for the future formalization of mock theta functions, modular forms, and the diverse algebraic structures that underpin their applications across mathematics and physics.
Problem
The theory of q-series and basic hypergeometric series connects combinatorics, number theory, and representation theory, but formalizing it requires reconciling formal algebraic identities with analytic convergence and handling many equivalent notational conventions.
Approach
The authors build reusable primitives in the Lean proof assistant on top of Mathlib, including q-Pochhammer symbols, q-binomial coefficients, and Bailey's Lemma, and design scalable structures for finite/infinite products and controlled limits via summation filters. They work over strongly non-archimedean complete rings with topologically nilpotent q to make convergence explicit. Formal proofs coordinate multiple normalizations (reindexing, unit multiplication, formal power series). An AI system (AxiomProver) assisted with intermediate lemmas and routine steps, with all theorems certified by the Lean kernel.
Results
Fully verified Lean proofs are given for the Jacobi Triple Product formula and both Rogers-Ramanujan identities, plus the Pentagonal Number Theorem and Jacobi's identity as corollaries. The work establishes a computational foundation for future formalization of modular forms and mock theta functions.
