Abstract

This entry to the Archive of Formal Proofs formalises the Rogers-Ramanujan Identities. The formalisation follows the elegant proof given in Andrews and Eriksson Integer Partitions, using the Jacobi triple product.

BibTeX

@article{Rogers_Ramanujan-AFP,
  author  = {Manuel Eberl},
  title   = {The {R}ogers--{R}amanujan Identities},
  journal = {Archive of Formal Proofs},
  month   = {December},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Rogers_Ramanujan.html},
             Formal proof development},
  ISSN    = {2150-914x},
}