BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Sphere Packing Problem and AI-Assisted Formalizatio
 n
DTSTART:20260420T101500
DTEND:20260420T111500
DTSTAMP:20260414T222457Z
UID:e69d491c7321b5206e0a95abf196b9c32a2f8bd71bfac99eabf67cbb
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Maryna Viazovska and Auguste Poiroux - EPFL\n\nMaryna Via
 zovska - Abstract\nThe talk will present the path toward formalizing the s
 phere packing problem in dimensions 8 and 24. It will highlight the main m
 ilestones achieved so far\, the role of AI\, and the challenges arising in
  large-scale formalization projects.\n\nAuguste Poiroux - Abstract\nOver t
 he last year\, AI systems have progressed rapidly in mathematics and are b
 eginning to tackle conjectures and open problems. This progress is excitin
 g\, but it also raises a verification challenge. Sophisticated proofs\, wh
 ether written by humans or generated by AI\, require substantial expertise
  and time to check\, and AI increases this burden by producing candidate p
 roofs at scale. Formalization\, the translation of mathematical content in
 to proof assistant code\, provides a promising way forward. Manual formali
 zation\, however\, still requires substantial effort and expertise. Autofo
 rmalization\, using AI\, is now showing key progress in addressing this bo
 ttleneck. In roughly one year\, the state of the art has moved from barely
  formalizing undergraduate-level statements to automatically formalizing w
 hole papers and textbooks. In this talk\, I will present my work on the to
 pic at EPFL and Math\, Inc. More specifically\, I will discuss autoformali
 zation in the context of Sphere Packing in dimensions 8 and 24\, the verif
 ication of AI solutions to conjectures using autoformalization\, and the n
 ext steps in AI for mathematics.\n\nMore information\nhttps://aiformath.ep
 fl.ch/ \n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/67078120700
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR