Pith. sign in

REVIEW 1 major objections 1 minor 43 references

Custom Lean structures yield fully verified proofs of the Jacobi triple product and Rogers-Ramanujan identities.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.3

2026-07-03 18:12 UTC pith:HXB35JF2

load-bearing objection Lean formalization of q-Pochhammer symbols and Rogers-Ramanujan identities gives a reusable library but leaves the analytic convergence details thin. the 1 major comments →

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

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

Kenny Lau , Seewoo Lee , Ken Ono This is my paper
classification math.NT math.COmath.LO
keywords q-seriesRogers-Ramanujan identitiesJacobi triple productLean proof assistantBailey's lemmaq-Pochhammer symbolsq-binomial coefficientsbasic hypergeometric series
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper constructs formal primitives in the Lean proof assistant for the theory of q-series. It defines structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's lemma that handle both algebraic manipulation and convergence requirements. These primitives are then used to produce machine-checked proofs of the Jacobi triple product formula and the Rogers-Ramanujan identities. The work positions these proofs as benchmarks that open a path to formalizing further objects such as mock theta functions and modular forms.

Core claim

By building scalable Lean structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's lemma that reconcile formal algebraic identities with analytic convergence properties, the authors obtain fully verified proofs of the Jacobi triple product formula and the Rogers-Ramanujan identities.

What carries the argument

Custom Lean structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's lemma that reconcile algebraic identities with analytic convergence.

Load-bearing premise

The custom Lean structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's lemma correctly reconcile formal algebraic identities with analytic convergence properties without introducing hidden assumptions about limits or convergence.

What would settle it

Discovery of a Lean code error that allows an algebraically invalid q-identity to pass verification, or a numerical mismatch between the formalized Rogers-Ramanujan sums and their known analytic values.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The same structures support formalization of mock theta functions and modular forms.
  • The proofs establish technical benchmarks for q-series formalization.
  • A rigorous computational foundation is supplied for applications in combinatorics, number theory, and representation theory.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The structures could be ported to other proof assistants to verify additional partition identities.
  • Verified q-series primitives might be applied to check specific conjectures arising in class field theory.
  • The approach opens a route to formal verification of further basic hypergeometric identities beyond the two benchmarks treated here.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 1 minor

Summary. The paper describes the formalization in Lean of q-series theory, focusing on scalable structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's Lemma to reconcile algebraic identities with analytic convergence. It claims to deliver fully verified proofs of the Jacobi Triple Product formula and the Rogers-Ramanujan identities as benchmarks for the field.

Significance. If the formalization is sound, the machine-checked proofs of these classical benchmark identities provide a rigorous computational foundation that could support future formalizations of mock theta functions, modular forms, and related structures in number theory and representation theory.

major comments (1)
  1. [Abstract] The central claim requires that the custom Lean structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's Lemma correctly reconcile algebraic identities with analytic convergence properties. The abstract states this reconciliation is addressed but provides no indication of how the radius of convergence (typically |q|<1) is formalized or whether the definitions treat the identities as purely algebraic equalities that hold only conditionally.
minor comments (1)
  1. [Abstract] The abstract refers to 'similar primitives' without enumeration or reference to their definitions or roles in the proofs.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and address the concern about the abstract's description of how algebraic and analytic aspects are reconciled in the formalization.

read point-by-point responses

  1. Referee: [Abstract] The central claim requires that the custom Lean structures for q-Pochhammer symbols, q-binomial coefficients, and Bailey's Lemma correctly reconcile algebraic identities with analytic convergence properties. The abstract states this reconciliation is addressed but provides no indication of how the radius of convergence (typically |q|<1) is formalized or whether the definitions treat the identities as purely algebraic equalities that hold only conditionally.

    Authors: The Lean structures are defined algebraically inside the ring of formal power series (or Laurent series) over the rationals, so that the identities hold unconditionally as equalities of formal series. The radius of convergence |q|<1 appears only when these formal identities are specialized to analytic functions; it is not encoded in the type definitions themselves. This separation is standard in the q-series literature and is explained in the body of the paper (particularly the sections on the Lean implementation of q-Pochhammer symbols and the statement of Bailey's Lemma). We agree that the abstract is too terse on this distinction and will revise it to state explicitly that the formalization is algebraic while convergence is imposed at the level of interpretation. revision: yes

Circularity Check

0 steps flagged

Formal Lean proofs are axiomatically verified with no circular derivation chain.

full rationale

The paper presents machine-checked proofs in the Lean proof assistant of the Jacobi Triple Product formula and Rogers-Ramanujan identities. These are constructed from explicitly defined primitives (q-Pochhammer symbols, q-binomial coefficients, Bailey's Lemma) whose algebraic identities are verified directly against Lean's axioms. No step reduces a claimed result to a fitted parameter, self-citation, or input by construction; the verification process itself serves as the independent benchmark. The work is self-contained as a formalization effort and does not rely on empirical predictions or ansatzes that could introduce circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Insufficient information from abstract only; no free parameters, axioms, or invented entities can be identified.

pith-pipeline@v0.9.1-grok · 5731 in / 1037 out tokens · 25880 ms · 2026-07-03T18:12:52.907804+00:00 · methodology

0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages · 2 internal anchors

  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, 31

    work page 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

    work page 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, 14, 19, 26, 27, 31

    work page 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

    work page 1976

  5. [5]

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

    work page 2004

  6. [6]

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

    work page 1949

  7. [7]

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

    work page 1982

  8. [8]

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

    work page 1991

  9. [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, 31

    work page 2017

  10. [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

    work page 2020

  11. [11]

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

    work page doi:10.1142/7252 2009

  12. [12]

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

    work page 1955

  13. [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

    work page 2015

  14. [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

    work page 2005

  15. [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

    work page 1997

  16. [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

    work page 1985

  17. [17]

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

    work page 1988

  18. [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

    work page 2004

  19. [19]

    Automatic Textbook Formalization

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

    work page internal anchor Pith review Pith/arXiv arXiv

  20. [20]

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

    work page 2016

  21. [21]

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

    work page internal anchor Pith review Pith/arXiv arXiv 2004

  22. [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

    work page arXiv 2025

  23. [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. 6

    work page 2002

  24. [24]

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

    work page

  25. [25]

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

    work page 2020

  26. [26]

    V. G. Kac, Infinite-Dimensional Lie Algebras , 3rd ed., Cambridge Univ. Press, Cambridge, 1990. 3 36 KENNY LAU, SEEWOO LEE, AND KEN ONO

    work page 1990

  27. [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

    work page 2004

  28. [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

    work page 2020

  29. [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. 6

    work page 2024

  30. [30]

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

    work page 2024

  31. [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. 6

    work page 2024

  32. [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. 31

    work page 1972

  33. [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

    work page 2004

  34. [34]

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

    work page

  35. [35]

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

    work page 1919

  36. [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. 31

    work page 1972

  37. [37]

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

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

    work page 1974

  38. [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

    work page 1917

  39. [39]

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

    work page 2017

  40. [40]

    Selsam, S

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

    work page arXiv 2001

  41. [41]

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

    work page 1929

  42. [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

    work page 1992

  43. [43]

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

    D. Zagier, Elliptic Modular Forms , 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, 67–84. 3 Axiom Math, 124 University A venue, Palo Alto, CA 94301 Email address : kenny@axiommath.ai Department of Mathematics, University of California—Berkeley, Berkeley, CA 94720 Email...

    work page 2008