BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Advancing Mathlib. Building a Curated Mathematical Library for the
  Future [HCM Workshop/Conference]
DTSTART:20270426T050000Z
DTEND:20270430T200000Z
DTSTAMP:20261021T084200Z
UID:indico-event-1554@math-events.uni-bonn.de
CONTACT:hcm-program@uni-bonn.de
DESCRIPTION:Formalisation of mathematics has seen a recent explosion of ac
 tivity. The Lean proof assistant has been used to formalise Fields-medal w
 inning mathematics and papers in the Annals of mathematics. Some papers ha
 ve been formalised before their referee report arrived\, or even before th
 e final manuscript was submitted. Formalisation has great potential to cha
 nge how mathematics is done. Scaling to "research papers can routinely be 
 formalised" requires library building: adding key definitions and building
  supporting theory around them.\nDuring this workshop\, we will focus on a
 dvancing Mathlib\, Lean's curated integrated library of formalized mathema
 tics. Most of the time is reserved for working in small groups\, on new or
  pre-existing projects adding to Mathlib. There will be time to discuss cr
 oss-cutting concerns\, a social event and time to connect as a community. 
 Participants are expected to have prior experience in contributing to Math
 lib.\nThe deadline for the application for participation is December 18th
 \, 2026.\nOur Global Mobility Fellowships provide participation opportunit
 ies for selected researchers and PhD students from countries of the Global
  South in the Special Topic Schools of the Hausdorff School for Mathematic
 s. For more information\, please visit our website.\nScientific Organize
 rs:\n\nFloris van Doorn (University of Bonn)\nMichael Rothgang (University
  of Bonn)\n\n\nhttps://math-events.uni-bonn.de/event/1554/
LOCATION:Poppelsdorfer Allee 45\, 1\, EG\, Lecture room - HIM PA82 (HIM)
URL:https://math-events.uni-bonn.de/event/1554/
END:VEVENT
END:VCALENDAR