Pith. sign in

REVIEW 5 minor 43 references

Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond

T0 review · 0 major / 5 minor · reviewed 2026-07-14 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Machine-checked proofs of the Jacobi triple product and Rogers–Ramanujan identities rest on a new class of non-archimedean rings that make infinite q-products converge.

desk verdict Solid Lean library that actually generalizes the classical q-series benchmarks; the new ring class is a design choice, not a correctness hole. read the letter →

arxiv 2607.01544 v2 pith:HXB35JF2 submitted 2026-07-01 math.NT math.COmath.LO

Kenny Lau , Seewoo Lee , Ken Ono This is my paper
classification math.NTmath.COmath.LO MSC 68V2068V1505A30
keywords q-seriesRogers-RamanujanidentitiesJacobitripleproductformalproofBailey'slemmaq-Pochhammersymbolsnon-archimedeanrings
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper builds a formal library of q-series primitives—q-Pochhammer symbols, q-binomial coefficients, and Bailey pairs—so classical identities can be stated and proved as equalities of formal series or convergent products inside a proof assistant. It introduces strongly non-archimedean rings to guarantee that infinite products of the form (1 + a_n) converge whenever a_n tends to zero and the base is topologically nilpotent, reconciling algebraic manipulation with analytic hypotheses. With that foundation it supplies fully verified proofs of the Jacobi triple product and both Rogers–Ramanujan sum-product identities, valid in complete strongly non-archimedean rings and therefore in the classical complex setting. The same development yields Euler’s pentagonal-number theorem and Jacobi’s cubic identity as corollaries. The work is offered as reusable infrastructure for later formalization of mock theta functions, modular forms, and related algebraic structures.

What carries the argument

Strongly non-archimedean rings (topological rings whose open additive subrngs form a neighborhood basis of zero) together with Bailey’s lemma on pairs of sequences; the former guarantees unconditional multipliability of products (1 + a_n) when a_n tends to zero, while the latter systematically generates the Rogers–Ramanujan series from elementary Bailey pairs.

What would settle it

Exhibit a complete non-archimedean ring that is not strongly non-archimedean yet still multiplies every product (1 + a_n) with a_n → 0, or re-check the formal artifact and find that the kernel rejects the proofs of the Jacobi triple product or either Rogers–Ramanujan identity.

Watch

Extended reading notes

Core claim

Fully kernel-checked formal proofs of the Jacobi triple product identity and the two Rogers–Ramanujan sum-product identities have been constructed; they hold for complete strongly non-archimedean rings with topologically nilpotent q and specialize to the classical statements over the complex numbers.

Load-bearing premise

The claim rests on the newly defined class of strongly non-archimedean rings being the right minimal setting that makes infinite products of the form (1 + a_n) converge whenever a_n tends to zero.

Editorial extensions

If this is right

  • The same library yields machine-checked forms of Euler’s pentagonal-number theorem and Jacobi’s identity for the cube of the Euler function.
  • Future formalizations of mock theta functions and modular forms can reuse the q-Pochhammer and Bailey infrastructure.
  • Partition congruences such as Ramanujan’s p(5n + 4) ≡ 0 mod 5 become reachable once the Jacobi triple product is available.
  • The algebraic setting opens the door to p-adic modular forms and modular forms over general rings.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The strongly non-archimedean ring class may become a standard primitive for formal non-archimedean analysis beyond q-series.
  • The partial universal property used to drop the “strong” hypothesis for purely nilpotent identities could simplify other formalizations that mix formal and topological series.
  • With Bailey’s lemma in place, systematic generation of further Rogers–Ramanujan-type identities becomes a short formal exercise rather than a multi-page calculation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. The paper develops a Lean/mathlib library for q-series, introducing q-Pochhammer symbols, q-binomials, q-hypergeometric series, Bailey pairs, and Bailey’s Lemma over commutative rings with topology. To reconcile algebraic identities with convergence, it defines StrongNonarchimedeanRing (open subrngs form a neighborhood basis of 0) and a total-degree multivariate Laurent series via Hahn series. It supplies fully kernel-checked proofs of the Jacobi triple product (Thm 1.1.1 / 4.1.4) and both Rogers–Ramanujan identities (Thm 1.1.2; first_/second_rogers_ramanujan) for complete strongly non-archimedean rings with topologically nilpotent q, with further specialization to ordinary NonarchimedeanRing via a partial universal property of power series (§5.3, Thm 3.7.2). Corollaries include Euler’s pentagonal number theorem and Jacobi’s cubic identity. The repository is public; AxiomProver assisted intermediate lemmas that were re-checked by the kernel.

Significance. This is a substantial, reusable formal foundation for classical q-series. Machine-checked proofs of Jacobi triple product and both Rogers–Ramanujan identities, stated in a ring-theoretic generality that specializes to the classical complex case, are genuine benchmarks. The public artifact, explicit comparison with prior Isabelle and RepoProver formalizations, and the infrastructure (Bailey pairs, hypergeometric transformations, functoriality of infinite products) make the work immediately usable for partition congruences, modular forms, and further identities. The StrongNonarchimedeanRing class and counter-example (Thm 9.2.2–9.2.3) are carefully motivated design choices rather than ad-hoc gaps. Credit is due for separating algebraic skeletons from analytic hypotheses and for documenting AI-assisted steps without claiming them as black-box proofs.

minor comments (5)
  1. §2.1.3 and Def. 3.3.1: a one-sentence comparison of StrongNonarchimedeanRing with Huber rings / linear topologies (already mentioned in Ex. 3.3.3) would help readers place the new class relative to existing non-archimedean literature.
  2. §4.1, (4.1.2)–(4.1.3): the two sign conventions for the Jacobi product (jacobi_triple_product vs jacobi_triple_product') are useful; a short remark on which form is preferred for modular-form applications would improve usability.
  3. §8: the AxiomProver appendix is valuable for reproducibility; a single table listing which theorems were AI-proposed versus human-designed would make the division of labor clearer without changing the mathematical claims.
  4. Notation 3.2.6 and the “unsafe” open QTheoryUnsafe: a brief warning in the main text (not only the code) that the abbreviated (a)_n notation is fragile would reduce user error.
  5. References: the comparison with Eberl’s Isabelle formalizations [29–31] and RepoProver is good; adding a pointer to any subsequent mathlib PRs (if any) would help readers track upstreaming.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: classical identities are derived from independent definitions and machine-checked lemmas, not assumed or fitted.

full rationale

This is a formalization paper whose central claims are fully kernel-checked Lean proofs of the classical Jacobi triple product (Thm 1.1.1 / 4.1.4) and Rogers–Ramanujan identities (Thm 1.1.2 / first_ and second_rogers_ramanujan). The derivation chain proceeds from explicit definitions of q-Pochhammer symbols, q-binomials, Bailey pairs and Bailey’s lemma (Defs 3.2.4–3.2.5, 3.6.1, Lemmas 3.6.3–3.6.4), through algebraic identities (q-binomial theorem, Heine, q-Gauss, q-Pfaff–Saalschütz) and the newly introduced StrongNonarchimedeanRing class (Def 3.3.1, Thm 3.3.5 with counter-example Thm 9.2.2–9.2.3), without ever taking the target equalities as hypotheses. The identities themselves are external classical benchmarks; the formal statements specialize to the usual complex-analytic forms under the stated topological hypotheses. Self-references are only to the authors’ own Lean library infrastructure, which is publicly machine-checked rather than assumed. No fitted parameters, self-definitional loops, uniqueness theorems imported from prior author work, or renaming of known empirical patterns appear. The paper is therefore self-contained against external mathematical benchmarks and exhibits zero circularity of the kinds enumerated.

Assumptions & free parameters 0 free parameters · 3 assumptions · 3 invented entities

No numerical free parameters. The work rests on standard commutative-ring and topological-ring axioms plus the authors’ definition of StrongNonarchimedeanRing and the junk-value conventions for inverses and infinite products. The invented ring class and series construction are the main novel entities; both are given explicit Lean definitions and counter-examples that justify their necessity.

assumptions (3)
  • standard math All rings are commutative; N contains 0 (Lean convention).
    Stated in §2.1.1; used throughout the typeclass hierarchy.
  • domain assumption A complete strongly non-archimedean ring admits unconditional multipliability of (1+a_n) whenever a_n o0.
    Theorem 3.3.5 / multipliable_one_add_of_tendsto_zero; the central existence lemma for (a;q)_∞.
  • standard math mathlib’s HasSum / tsum / tprod and Hahn-series infrastructure behave as documented.
    Imported background; the paper builds multivariate Laurent series on top of it.
invented entities (3)
  • StrongNonarchimedeanRing
    purpose: Guarantee that products ∏(1+a_n) converge when a_n o0, which ordinary non-archimedean rings do not.
    Definition 3.3.1; counter-example in §9.2 shows the stronger axiom is necessary for the q-Pochhammer product.
  • Total-degree multivariate Laurent series (via Hahn series)
    purpose: Allow negative exponents while retaining a complete non-archimedean topology and coefficient extraction.
    §2.1.5; used to state and prove the general Jacobi triple product without forcing invertibility of a.
  • bInv (both-sided inverse with junk value 1)
    purpose: Avoid carrying unit proofs through every algebraic identity involving inverses of Pochhammer symbols.
    §2.2.1; used extensively in Bailey and hypergeometric lemmas.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond." pith.science (2026). https://pith.science/paper/HXB35JF2

@misc{pith2026260701544,
  author       = {Pith},
  title        = {Pith review of: Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HXB35JF2}},
  note         = {Machine review of arXiv:2607.01544}
}
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. AxiomProver was used to produce the formalizations in this paper.

Review history (2 revisions) →

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

43 extracted references · 4 linked inside Pith

  1. [1]

    G. E. Andrews, An analytic generalization of the Rogers–Ramanujan identities for odd moduli , Proc. Natl. Acad. Sci. USA 71 (1974), no. 10, 4082–4085. 2, 32

    1974

  2. [2]

    G. E. Andrews, Problems and prospects for basic hypergeometric functions , in R. Askey (ed.), Theory and Application of Special Functions , Academic Press, New York, 1975, 191–224. 2

    1975

  3. [3]

    G. E. Andrews, q-Series: Their development and application in analysis, number theory, combinatorics, physics, and computer algebra , American Mathematical Soc., 1986 2, 15, 20, 27, 28, 32

    1986

  4. [4]

    G. E. Andrews, The Theory of Partitions , Encyclopedia of Mathematics and its Applications, vol. 2, Addison– Wesley, Reading, MA, 1976; reprinted by Cambridge Univ. Press, 1998. 1, 2, 3

    1976

  5. [5]

    G. E. Andrews and K. Eriksson. Integer Partitions . Cambridge University Press, 2004. 7

    2004

  6. [6]

    W. N. Bailey, Identities of the Rogers–Ramanujan type , Proc. London Math. Soc. (2) 50 (1949), 1–10. 3, 32

    1949

  7. [7]

    R. J. Baxter, Exactly Solved Models in Statistical Mechanics , Academic Press, London, 1982. 3

    1982

  8. [8]

    B. C. Berndt. Ramanujan ’s Notebooks. Springer New York, 1991. 7, 32

    1991

Show all 43 references
  1. [9]

    Bringmann, A

    K. Bringmann, A. Folsom, K. Ono, and L. Rolen, Harmonic Maass Forms and Mock Modular Forms: Theory and Applications , American Mathematical Society Colloquium Publications, Vol. 64, American Mathematical Society, Providence, RI, 2017. 2, 32

    2017

  2. [10]

    Buzzard, Division by zero in type theory: a F AQ , Xena Project blog, 2020

    K. Buzzard, Division by zero in type theory: a F AQ , Xena Project blog, 2020. https://xenaproject.wordpress. com/2020/07/05/division-by-zero-in-type-theory-a-faq/ . 5

    2020

  3. [11]

    Chan, H. H. (2009). Analytic Number Theory for Undergraduates. In Monographs in number theory. https://doi.org/10.1142/7252 25, 33

    2009 doi

  4. [12]

    E. A. Coddington and N. Levinson, Theory of Ordinary Differential Equations , McGraw–Hill, New York, 1955

    1955

  5. [13]

    de Moura, S

    L. de Moura, S. Kong, J. A vigad, F. van Doorn, and J. von Raumer, The Lean theorem prover (system description), in Automated Deduction – CADE-25 , Lecture Notes in Computer Science, vol. 9195, Springer, Cham, 2015, 378–388. 3

    2015

  6. [14]

    Diamond and J

    F. Diamond and J. Shurman, A First Course in Modular Forms , Graduate Texts in Mathematics, vol. 228, Springer, New York, 2005. 3 THE ROGERS–RAMANUJAN IDENTITIES 37

    2005

  7. [15]

    Di Francesco, P

    P. Di Francesco, P. Mathieu, and D. Sénéchal, Conformal Field Theory , Graduate Texts in Contemporary Physics, Springer, New York, 1997. 3

    1997

  8. [16]

    Eichler and D

    M. Eichler and D. Zagier, The Theory of Jacobi Forms , Progress in Mathematics, Vol. 55, Birkhäuser Boston, Boston, MA, 1985. 2

    1985

  9. [17]

    I. B. Frenkel, J. Lepowsky, and A. Meurman, Vertex Operator Algebras and the Monster , Pure and Applied Mathematics, Academic Press, Boston, 1988. 3

    1988

  10. [18]

    Gasper and M

    G. Gasper and M. Rahman, Basic Hypergeometric Series , 2nd ed., Encyclopedia of Mathematics and its Applications, vol. 96, Cambridge Univ. Press, Cambridge, 2004. 1, 3

    2004

  11. [19]

    Gloeckle, A

    F. Gloeckle, A. Rammal, C. Arnal, R. Munos, V. Cabannes, G. Synnaeve, A.Hayat, Automatic Textbook Formalization, arXiv preprint arXiv:2604.03071. 6

    arXiv

  12. [20]

    M. J. Griffin, K. Ono, and S. O. Warnaar, A framework of Rogers–Ramanujan identities and their arithmetic properties, Duke Math. J. 165 (2016), no. 8, 1475–1527. 3, 32

    2016

  13. [21]

    Gabber, O., and Ramero, L, Foundations for almost ring theory , arXiv preprint arXiv:math/0409584 (2004). 23

    2004 arXiv

  14. [22]

    Grinberg, An introduction to algebraic combinatorics , arXiv preprint arXiv:2506.00738 (2025)

    D. Grinberg, An introduction to algebraic combinatorics , arXiv preprint arXiv:2506.00738 (2025). 6

    2025 arXiv

  15. [23]

    Nipkow, M

    T. Nipkow, M. Wenzel, and L. C. Paulson, eds. Isabelle/HOL: a proof assistant for higher-order logic . Berlin, Heidelberg: Springer Berlin Heidelberg, 2002. 7

    2002

  16. [24]

    C. G. J. Jacobi, Fundamenta nova theoriae functionum ellipticarum , Sumtibus Fratrum Borntraeger, Re- giomonti, 1829. 2

  17. [25]

    W. P. Johnson. An introduction to q-analysis. Vol. 134. American Mathematical Soc., 2020

    2020

  18. [26]

    V. G. Kac, Infinite-Dimensional Lie Algebras , 3rd ed., Cambridge Univ. Press, Cambridge, 1990. 3

    1990

  19. [27]

    Lepowsky and H

    J. Lepowsky and H. S. Li, Introduction to Vertex Operator Algebras and Their Representations , Progress in Mathematics, vol. 227, Birkhäuser, Boston, 2004. 3

    2004

  20. [28]

    The mathlib Community, The Lean mathematical library, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , ACM, New York, 2020, 367–381. 3

    2020

  21. [29]

    Eberl, Theta Functions, Archive of Formal Proofs , December 2024, https://isa-afp.org/entries/Theta_ Functions.html, Formal proof development

    M. Eberl, Theta Functions, Archive of Formal Proofs , December 2024, https://isa-afp.org/entries/Theta_ Functions.html, Formal proof development. 7

    2024

  22. [30]

    M. Eberl, The Partition Function and the Pentagonal Number Theorem, Archive of Formal Proofs , April 2025, https://isa-afp.org/entries/Pentagonal_Number_Theorem.html, Formal proof development. 7

    2025

  23. [31]

    Eberl, The Rogers–Ramanujan Identities, Archive of Formal Proofs , December 2024, https://isa-afp.org/ entries/Rogers_Ramanujan.html, Formal proof development

    M. Eberl, The Rogers–Ramanujan Identities, Archive of Formal Proofs , December 2024, https://isa-afp.org/ entries/Rogers_Ramanujan.html, Formal proof development. 7

    2024

  24. [32]

    N. M. Katz, P-adic properties of modular schemes and modular forms. Modular Functions of One Variable III: Proceedings International Summer School University of Antwerp, RUCA July 17–August 3, 1972. Berlin, Heidelberg: Springer Berlin Heidelberg, 1973. 69-190. 33

    1972

  25. [33]

    Ono, The Web of Modularity: Arithmetic of the Coefficients of Modular Forms and q-series, CBMS Regional Conference Series in Mathematics, vol

    K. Ono, The Web of Modularity: Arithmetic of the Coefficients of Modular Forms and q-series, CBMS Regional Conference Series in Mathematics, vol. 102, Amer. Math. Soc., Providence, RI, 2004. 3

    2004

  26. [34]

    L. J. Rogers, Second memoir on the expansion of certain infinite products , Proc. London Math. Soc. 25 (1894), 318–343. 2

  27. [35]

    L. J. Rogers and S. Ramanujan, Proof of certain identities in combinatory analysis , Proc. Cambridge Philos. Soc. 19 (1919), 211–216. 2

    1919

  28. [36]

    Serre, Formes modulaires et fonctions zêta p-adiques

    J.-P. Serre, Formes modulaires et fonctions zêta p-adiques. Modular Functions of One Variable III: Proceed- ings International Summer School University of Antwerp, RUCA July 17–August 3, 1972. Berlin, Heidelberg: Springer Berlin Heidelberg, 1973. 191-268. 33

    1972

  29. [37]

    Schoeneberg, Elliptic Modular Functions: An Introduction , Springer, Berlin, 1974

    B. Schoeneberg, Elliptic Modular Functions: An Introduction , Springer, Berlin, 1974. 3

    1974

  30. [38]

    Schur, Ein Beitrag zur additiven Zahlentheorie und zur Theorie der Kettenbrüche , Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften zu Berlin (1917), 302–321

    I. Schur, Ein Beitrag zur additiven Zahlentheorie und zur Theorie der Kettenbrüche , Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften zu Berlin (1917), 302–321. 2

    1917

  31. [39]

    A. V. Sills, An Invitation to the Rogers–Ramanujan Identities , CRC Press, Boca Raton, FL, 2017. 1, 3, 32

    2017

  32. [40]

    Selsam, S

    D. Selsam, S. Ullrich, and L. de Moura, Tabled typeclass resolution, arXiv preprint arXiv:2001.04301 (2020). 3

    2001 arXiv

  33. [41]

    G. N. Watson, A new proof of the Rogers–Ramanujan identities , J. London Math. Soc. 4 (1929), 4–9. 18

    1929

  34. [42]

    H. S. Wilf, D. Zeilberger. An algorithmic proof theory for hypergeometric (ordinary and “q”) multisum/integral identities, Inventiones mathematicae 108, no. 1 (1992), 575-633

    1992

  35. [43]

    Zagier, Elliptic Modular Forms and Their Applications , in The 1-2-3 of Modular Forms (J

    D. Zagier, Elliptic Modular Forms and Their Applications , in The 1-2-3 of Modular Forms (J. H. Bruinier, G. van der Geer, G. Harder, and D. Zagier, eds.), Universitext, Springer, Berlin, 2008, 1–103. 3 38 KENNY LAU, SEEWOO LEE, AND KEN ONO Axiom Math, 124 University A venue, ...

    2008

Pith tools

Reviewed July 14, 2026 · model on record in the stance chip above.