NUMBER THEORY SEMINAR - Formalizing Jacobi's four-squares theorem in Lean 4

Jacobi's theorem provides a closed formula for the number of representations of an integer as a sum of four squares, and can be proved as an introductory application of the theory of classic modular forms. In this talk, we outline its proof using Eisenstein and theta series. We then discuss the challenges of formalizing this proof in the Lean 4 proof assistant, using an algebraic strategy to derive the key dimension bound for the relevant space of modular forms from the valence formula for the full modular group.