This repository accompanies the paper Formalized q-series: The Rogers-Ramanujan Identities and Beyond.
This repository contains a Lean formalization of the Rogers–Ramanujan Identities as well as extra entities such as the Pentagonal Number Theorem, Jacobi's Identity involving triangular numbers, and useful counterexamples.
This repository depends on Lean and Mathlib version 4.31.0.