BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Road to Formalising 8-Dimensional Sphere Packing in Lean - Sid
 harth Hariharan (Carnegie Mellon University)
DTSTART:20251009T160000Z
DTEND:20251009T170000Z
UID:TALK237553@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:In 2022\, Maryna Viazovska was awarded the Fields Medal for an
  outstanding achievement: solving the sphere packing problem in dimension 
 8. The ingenuity of Viazovska's solution stems from her combination of tec
 hniques from the apparently unrelated theories of radial Schwartz function
 s and modular forms to construct a so-called "magic function"\, using whic
 h one can show that the density of the E₈ sphere packing is an upper-bou
 nd for all sphere packings in dimension 8.\n\nAround 18 months ago\, I emb
 arked on a venture to really put the capabilities of Lean to test: I began
  a project to formalise Viazovska's groundbreaking solution. Never before 
 has work that is both as recent and as highly acclaimed as Viazovska's bee
 n formalised\, and if this project succeeds\, it will be an important mile
 stone for the formalisation movement.\n\nThis talk is based on joint (and 
 ongoing) work by Birkbeck\, Hariharan\, Ma\, Mehta\, Lee\, Viazovska\, and
  open-source contributors.\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting htt
 ps://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\
 n\nMeeting ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR