BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:Some practical problems in formalising mathematics
  and how to solve them - Dr Manuel Eberl (Universi
 ty of Innsbruck)
DTSTART;TZID=Europe/London:20230209T170000
DTEND;TZID=Europe/London:20230209T180000
UID:TALK193211AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/193211
DESCRIPTION:In this talk\, I give a very high-level overview a
 bout some recent work concerning the formalisation
  of mathematics in the interactive theorem prover 
 Isabelle/HOL. I start with a very brief look at wh
 at Isabelle/HOL is and what formalised mathematics
  looks like. Then I show two particular problems t
 hat I encountered and how I solved them\, namely a
 symptotic estimates of real-valued functions and c
 omplicated integration contours arising in Analyti
 c Number Theory.\n\n\nWATCH ONLINE HERE: https://w
 ww.microsoft.com/en-gb/microsoft-teams/join-a-meet
 ing?rtc=1 Meeting ID: 379 992 884 209 Passcode: TY
 R8 Sh
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
CONTACT:Angeliki Koutsoukou-Argyraki
END:VEVENT
END:VCALENDAR