BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Formalisation\, AI and the role of mathlib [MPIM]
DTSTART:20261030T144500Z
DTEND:20261030T154500Z
DTSTAMP:20261030T234400Z
UID:indico-event-1684@math-events.uni-bonn.de
DESCRIPTION:Speakers: Michael Rothgang (Universität Bonn)\n\nMathematics 
 and AI Discussion Seminar\nDigitising or formalising mathematics refers to
  translating mathematical arguments from natural language (e.g. English) i
 nto a computer-readable format: this makes it possible to verify proofs wi
 th certainty\, often improves mathematical understanding\, can transform p
 eer-review and enables new levels of collaboration. Formalisation of mathe
 matics has come of age now: in recent years and months\, there has been sp
 ectacular progress in formalising research-level mathematics in diverse fi
 elds. In fact\, recent AI-assisted breakthroughs (such as\, on the Navier-
 Stokes equations) have been enabled through formalisation.I will explain w
 hat the excitement is about and give an idea of the current state of the a
 rt. I will discuss what this means for human formalisation and the mathlib
  library in particular: despite the rapidly changing ecosystem\, they stil
 l take an important role\, for the ecosystem and human understanding.\nMor
 e information about the Mathematics and AI seminar can be found on its web
 site:https://challeckdube.github.io/mathematics-and-ai-seminar.html\n\nhtt
 ps://math-events.uni-bonn.de/event/1684/
LOCATION:MPIM\, Vivatsgasse\,  7 - Lecture Hall (Max Planck Institute for 
 Mathematics)
URL:https://math-events.uni-bonn.de/event/1684/
END:VEVENT
END:VCALENDAR