Maryna Viazovska is launching a project to formalize a proof of her well-known result that the E_8 lattice is the optimal sphere packing in eight dimensions. The announcement can be found at https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Sphere-Packing/with/523951357 where you can also find a talk by Viazovska describing the project.

Among other things, the project will develop some of the classical theory of modular forms and complex analysis, which is only partially in Lean's Mathlib at present. For instance, Cauchy's theorem is only currently available for rectangular contours, which means that the valence formula for modular forms (which is usually proven using Cauchy's theorem applied to a non-rectangular contour) is not yet formalized.