This repository consists of LEAN code which defines modular forms and looks to prove that Eisenstein series satisfy these definitions. The code within is being organised in order to be added to mathlib. The relevant PR is: leanprover-community/mathlib3#8979 (see here for up-to-date code).