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:Formalizing algebraic number theory\, recent progr
ess and future challenges - Dr Alex J. Best (King'
s College London)
DTSTART;TZID=Europe/London:20230608T170000
DTEND;TZID=Europe/London:20230608T180000
UID:TALK196741AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/196741
DESCRIPTION:Most areas of mathematics present their own indivi
dual challenges from the perspective of formalizat
ion\, arguments that are perceived as routine and
obvious\, or simply well known or intuitive to pra
ctitioners\, that turn out to be far more difficul
t to express in a formal system.\nI'll present som
e recent formalization projects from my own area o
f mathematics\, concerning basic yet central topic
s in algebraic number theory\, such as class group
s and diophantine equations\, and local invariants
of elliptic curves.\nThese areas have until recen
tly seen relatively little attention from the pers
pective of formalization.\nA special attention wil
l be paid to aspects that have made these formaliz
ations tricky to complete and ways in which proof
assistants can be improved to ensure future formal
izations in these areas are shorter and closer to
the arguments used by those working in these field
s.
LOCATION:MR20 Centre for Mathematical Sciences
CONTACT:Angeliki Koutsoukou-Argyraki
END:VEVENT
END:VCALENDAR