Formalizing modular forms and the Valence Formula using LEAN. To open the LEAN live editor visit https://ferrandf.github.io/valenceformula/ The files done during this project are in src. Take into account we are using a specific version of LEAN. You can check it in the leanpkg.toml file.