The goal of this project is to formalize the many identities in Gradshteyn and Ryzhik's Table of Integrals, Series, and Products using the Lean theorem prover.
This will be a massive undertaking, but my current goal is to at least get through the first chapter.
The primary identities will be proven in chapter{n}.lean, while corresponding helper theorems will be proven in lemmas{n}.lean. The identities will be named according to the equation number in the book (currently the 7th edition).