BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Metaprogramming for the Formalizing Mathematician [HIM/HSM Special
  Topic School]
DTSTART:20270419T050000Z
DTEND:20270423T200000Z
DTSTAMP:20261025T145200Z
UID:indico-event-1555@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.\nScaling to "research papers can routinely be
  formalised" requires library building and improving the ergonomics of for
 malisation. Fortunately\, Lean can be extended using *metaprogramming*: th
 is can be used to recognise and fix problematic patterns in code (linter) 
 or to automate constructions currently done by hand.\nThis school offers a
 n introduction to metaprogramming\, allowing you to get hands-on experienc
 e under the guidance of expert tutors. A series of lectures will explain t
 he topic systematically\, with plenty of time left for problem-solving and
  first small projects. You can suggest your own project topic if you like.
 \nParticipants are expected to have experience with Lean\; no metaprogramm
 ing experience is required.\nThe deadline for the application for particip
 ation is December 18th\, 2026.\nOur Global Mobility Fellowships provide p
 articipation opportunities for selected researchers and PhD students from 
 countries of the Global South in the Special Topic Schools of the Hausdorf
 f School for Mathematics. For more information\, please visit our websit
 e.\nLecture series by:\n\nAnne Baanen (Mathlib Initiative)\nMario Carneiro
  (Chalmers University of Technology)\nJovan Gerbscheid (Cambridge)\nThomas
  Murrills (Mathlib Initiative)\nDamiano Testa (U Warwick)\nEric Wieser (Go
 ogle Deepmind)\n\nScientific Organizers:\n\nFloris van Doorn (University o
 f Bonn)\nMichael Rothgang (University of Bonn)\n\n\nhttps://math-events.un
 i-bonn.de/event/1555/
LOCATION:Poppelsdorfer Allee 45\, 1\, EG\, Lecture room - HIM PA82 (HIM)
URL:https://math-events.uni-bonn.de/event/1555/
END:VEVENT
END:VCALENDAR