BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:NUMBER THEORY SEMINAR - Formalizing Jacobi's four-squares theorem 
 in Lean 4
DTSTART:20260527T150000
DTEND:20260527T160000
DTSTAMP:20260527T120302Z
UID:e82f7465d36aefd62b2c1f720fbab4410ee64efd8c8846f38aa9f879
CATEGORIES:Conferences - Seminars
DESCRIPTION:Tito Sacchi   \nJacobi's theorem provides a closed formula f
 or 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 th
 eta series. We then discuss the challenges of formalizing this proof in th
 e Lean 4 proof assistant\, using an algebraic strategy to derive the key d
 imension bound for the relevant space of modular forms from the valence fo
 rmula for the full modular group. 
LOCATION:GR A3 32 https://plan.epfl.ch/?room==GR%20A3%2032
STATUS:CANCELLED
END:VEVENT
END:VCALENDAR