The Rogers–Ramanujan Identities

This entry formalises the Rogers--Ramanujan Identities: \begin{alignat*}{3} \sum_{k=-\infty}^\infty \frac{q^{k^2}}{\prod_{j=1}^k (1 - q^j)} &= \left(\,\prod_{n=0}^\infty (1 - q^{1+5n}) (1-q^{4+5n})\right)^{-1}\\ \sum_{k=-\infty}^\infty \frac{q^{k^2+k}}{\prod_{j=1}^k (1 - q^j)} &= \left(\,\prod_{n=0}^\infty (1 - q^{2+5n}) (1-q^{3+5n})\right)^{-1} \end{alignat*}

The formalisation follows the elegant proof given in Andrews and Eriksson Integer Partitions, using the Jacobi triple product.