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:20260525T040229Z
UID:e69d491c7321b5206e0a95abf196b9c32a2f8bd71bfac99eabf67cbb
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Maryna Viazovska and Auguste Poiroux - EPFL\nVideo of the
  talk\n\nMaryna Viazovska - Abstract\nThe talk will present the path towar
 d formalizing the sphere packing problem in dimensions 8 and 24. It will h
 ighlight the main milestones achieved so far\, the role of AI\, and the ch
 allenges arising in large-scale formalization projects.\n\nAuguste Poiroux
  - Abstract\nOver the last year\, AI systems have progressed rapidly in ma
 thematics and are beginning to tackle conjectures and open problems. This 
 progress is exciting\, but it also raises a verification challenge. Sophis
 ticated proofs\, whether written by humans or generated by AI\, require su
 bstantial expertise and time to check\, and AI increases this burden by pr
 oducing candidate proofs at scale. Formalization\, the translation of math
 ematical content into proof assistant code\, provides a promising way forw
 ard. Manual formalization\, however\, still requires substantial effort an
 d expertise. Autoformalization\, using AI\, is now showing key progress in
  addressing this bottleneck. In roughly one year\, the state of the art ha
 s moved from barely formalizing undergraduate-level statements to automati
 cally formalizing whole papers and textbooks. In this talk\, I will presen
 t my work on the topic at EPFL and Math\, Inc. More specifically\, I will 
 discuss autoformalization in the context of Sphere Packing in dimensions 8
  and 24\, the verification of AI solutions to conjectures using autoformal
 ization\, and the next steps in AI for mathematics.\n\nMore information\nh
 ttps://aiformath.epfl.ch/ \n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/67078120700
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR